:: BVFUNC24 semantic presentation
theorem Th1: :: BVFUNC24:1
for b
1 being non
empty set for b
2 being
Subset of
(PARTITIONS b1)for b
3, b
4, b
5, b
6, b
7, b
8, b
9 being
a_partition of b
1 holds
( b
2 = {b3,b4,b5,b6,b7,b8,b9} & b
3 <> b
4 & b
3 <> b
5 & b
3 <> b
6 & b
3 <> b
7 & b
3 <> b
8 & b
3 <> b
9 & b
4 <> b
5 & b
4 <> b
6 & b
4 <> b
7 & b
4 <> b
8 & b
4 <> b
9 & b
5 <> b
6 & b
5 <> b
7 & b
5 <> b
8 & b
5 <> b
9 & b
6 <> b
7 & b
6 <> b
8 & b
6 <> b
9 & b
7 <> b
8 & b
7 <> b
9 & b
8 <> b
9 implies
CompF b
3,b
2 = ((((b4 '/\' b5) '/\' b6) '/\' b7) '/\' b8) '/\' b
9 )
proof
let c
1 be non
empty set ;
let c
2 be
Subset of
(PARTITIONS c1);
let c
3, c
4, c
5, c
6, c
7, c
8, c
9 be
a_partition of c
1;
assume E2:
( c
2 = {c3,c4,c5,c6,c7,c8,c9} & c
3 <> c
4 & c
3 <> c
5 & c
3 <> c
6 & c
3 <> c
7 & c
3 <> c
8 & c
3 <> c
9 & c
4 <> c
5 & c
4 <> c
6 & c
4 <> c
7 & c
4 <> c
8 & c
4 <> c
9 & c
5 <> c
6 & c
5 <> c
7 & c
5 <> c
8 & c
5 <> c
9 & c
6 <> c
7 & c
6 <> c
8 & c
6 <> c
9 & c
7 <> c
8 & c
7 <> c
9 & c
8 <> c
9 )
;
E3:
CompF c
3,c
2 = '/\' (c2 \ {c3})
by BVFUNC_2:def 7;
E4:
c
2 \ {c3} = ({c3} \/ {c4,c5,c6,c7,c8,c9}) \ {c3}
by E2, ENUMSET1:56;
E5:
not c
4 in {c3}
by E2, TARSKI:def 1;
E6:
not c
5 in {c3}
by E2, TARSKI:def 1;
E7:
not c
6 in {c3}
by E2, TARSKI:def 1;
E8:
not c
7 in {c3}
by E2, TARSKI:def 1;
E9:
not c
8 in {c3}
by E2, TARSKI:def 1;
E10:
not c
9 in {c3}
by E2, TARSKI:def 1;
E11:
{c6,c7} \ {c3} = {c6,c7}
by E7, E8, ZFMISC_1:72;
{c4,c5,c6,c7,c8,c9} \ {c3} =
({c4} \/ {c5,c6,c7,c8,c9}) \ {c3}
by ENUMSET1:51
.=
({c4} \ {c3}) \/ ({c5,c6,c7,c8,c9} \ {c3})
by XBOOLE_1:42
.=
{c4} \/ ({c5,c6,c7,c8,c9} \ {c3})
by E5, ZFMISC_1:67
.=
{c4} \/ (({c5} \/ {c6,c7,c8,c9}) \ {c3})
by ENUMSET1:47
.=
{c4} \/ (({c5} \ {c3}) \/ ({c6,c7,c8,c9} \ {c3}))
by XBOOLE_1:42
.=
{c4} \/ (({c5} \ {c3}) \/ (({c6,c7} \/ {c8,c9}) \ {c3}))
by ENUMSET1:45
.=
{c4} \/ (({c5} \ {c3}) \/ (({c6,c7} \ {c3}) \/ ({c8,c9} \ {c3})))
by XBOOLE_1:42
.=
{c4} \/ (({c5} \ {c3}) \/ ({c6,c7} \/ {c8,c9}))
by E9, E10, E11, ZFMISC_1:72
.=
{c4} \/ ({c5} \/ ({c6,c7} \/ {c8,c9}))
by E6, ZFMISC_1:67
.=
{c4} \/ ({c5} \/ {c6,c7,c8,c9})
by ENUMSET1:45
.=
{c4} \/ {c5,c6,c7,c8,c9}
by ENUMSET1:47
.=
{c4,c5,c6,c7,c8,c9}
by ENUMSET1:51
;
then E12: c
2 \ {c3} =
({c3} \ {c3}) \/ {c4,c5,c6,c7,c8,c9}
by E4, XBOOLE_1:42
.=
{} \/ {c4,c5,c6,c7,c8,c9}
by XBOOLE_1:37
;
E13:
((((c4 '/\' c5) '/\' c6) '/\' c7) '/\' c8) '/\' c
9 c= '/\' (c2 \ {c3})
proof
let c
10 be
set ;
:: according to TARSKI:def 3
assume E14:
c
10 in ((((c4 '/\' c5) '/\' c6) '/\' c7) '/\' c8) '/\' c
9
;
then
c
10 in (INTERSECTION ((((c4 '/\' c5) '/\' c6) '/\' c7) '/\' c8),c9) \ {{} }
by PARTIT1:def 4;
then
( c
10 in INTERSECTION ((((c4 '/\' c5) '/\' c6) '/\' c7) '/\' c8),c
9 & not c
10 in {{} } )
by XBOOLE_0:def 4;
then consider c
11, c
12 being
set such that E15:
( c
11 in (((c4 '/\' c5) '/\' c6) '/\' c7) '/\' c
8 & c
12 in c
9 & c
10 = c
11 /\ c
12 )
by SETFAM_1:def 5;
c
11 in (INTERSECTION (((c4 '/\' c5) '/\' c6) '/\' c7),c8) \ {{} }
by E15, PARTIT1:def 4;
then
( c
11 in INTERSECTION (((c4 '/\' c5) '/\' c6) '/\' c7),c
8 & not c
11 in {{} } )
by XBOOLE_0:def 4;
then consider c
13, c
14 being
set such that E16:
( c
13 in ((c4 '/\' c5) '/\' c6) '/\' c
7 & c
14 in c
8 & c
11 = c
13 /\ c
14 )
by SETFAM_1:def 5;
c
13 in (INTERSECTION ((c4 '/\' c5) '/\' c6),c7) \ {{} }
by E16, PARTIT1:def 4;
then
( c
13 in INTERSECTION ((c4 '/\' c5) '/\' c6),c
7 & not c
13 in {{} } )
by XBOOLE_0:def 4;
then consider c
15, c
16 being
set such that E17:
( c
15 in (c4 '/\' c5) '/\' c
6 & c
16 in c
7 & c
13 = c
15 /\ c
16 )
by SETFAM_1:def 5;
c
15 in (INTERSECTION (c4 '/\' c5),c6) \ {{} }
by E17, PARTIT1:def 4;
then
( c
15 in INTERSECTION (c4 '/\' c5),c
6 & not c
15 in {{} } )
by XBOOLE_0:def 4;
then consider c
17, c
18 being
set such that E18:
( c
17 in c
4 '/\' c
5 & c
18 in c
6 & c
15 = c
17 /\ c
18 )
by SETFAM_1:def 5;
c
17 in (INTERSECTION c4,c5) \ {{} }
by E18, PARTIT1:def 4;
then
( c
17 in INTERSECTION c
4,c
5 & not c
17 in {{} } )
by XBOOLE_0:def 4;
then consider c
19, c
20 being
set such that E19:
( c
19 in c
4 & c
20 in c
5 & c
17 = c
19 /\ c
20 )
by SETFAM_1:def 5;
set c
21 =
(((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12);
E20:
dom ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) =
{c9,c4,c5,c6,c7,c8}
by BVFUNC14:41
.=
{c9} \/ {c4,c5,c6,c7,c8}
by ENUMSET1:51
.=
{c4,c5,c6,c7,c8,c9}
by ENUMSET1:55
;
E21:
dom ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) =
{c9,c4,c5,c6,c7,c8}
by BVFUNC14:41
.=
{c9} \/ {c4,c5,c6,c7,c8}
by ENUMSET1:51
.=
{c4,c5,c6,c7,c8,c9}
by ENUMSET1:55
;
E22:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
6 = c
18
by E2, BVFUNC14:40;
E23:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
4 = c
19
by E2, BVFUNC14:40;
E24:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
5 = c
20
by E2, BVFUNC14:40;
E25:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
7 = c
16
by E2, BVFUNC14:40;
E26:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
8 = c
14
by E2, BVFUNC14:40;
E27:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
9 = c
12
by E2, BVFUNC14:40;
E28:
for b
1 being
set holds
( b
1 in c
2 \ {c3} implies
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . b
1 in b
1 )
c
6 in dom ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by E21, ENUMSET1:def 4;
then E29:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
6 in rng ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by FUNCT_1:def 5;
c
4 in dom ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by E21, ENUMSET1:def 4;
then E30:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
4 in rng ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by FUNCT_1:def 5;
c
5 in dom ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by E21, ENUMSET1:def 4;
then E31:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
5 in rng ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by FUNCT_1:def 5;
c
7 in dom ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by E21, ENUMSET1:def 4;
then E32:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
7 in rng ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by FUNCT_1:def 5;
c
8 in dom ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by E21, ENUMSET1:def 4;
then E33:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
8 in rng ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by FUNCT_1:def 5;
c
9 in dom ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by E21, ENUMSET1:def 4;
then E34:
((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c
9 in rng ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by FUNCT_1:def 5;
E35:
rng ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) c= {(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c4),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c5),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c6),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c7),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c8),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c9)}
{(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c4),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c5),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c6),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c7),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c8),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c9)} c= rng ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
proof
let c
22 be
set ;
:: according to TARSKI:def 3
assume
c
22 in {(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c4),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c5),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c6),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c7),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c8),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c9)}
;
hence
c
22 in rng ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12))
by E29, E30, E31, E32, E33, E34, ENUMSET1:def 4;
end;
then E36:
rng ((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) = {(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c4),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c5),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c6),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c7),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c8),(((((((c4 .--> c19) +* (c5 .--> c20)) +* (c6 .--> c18)) +* (c7 .--> c16)) +* (c8 .--> c14)) +* (c9 .--> c12)) . c9)}
by E35, XBOOLE_0:def 10;
rng ((((((c4 .--> c19) +* (