let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)

for A, B, C, D being a_partition of Y st G = {A,B,C,D} & A <> B & A <> C & A <> D holds

CompF (A,G) = (B '/\' C) '/\' D

let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D being a_partition of Y st G = {A,B,C,D} & A <> B & A <> C & A <> D holds

CompF (A,G) = (B '/\' C) '/\' D

let A, B, C, D be a_partition of Y; :: thesis: ( G = {A,B,C,D} & A <> B & A <> C & A <> D implies CompF (A,G) = (B '/\' C) '/\' D )

assume that

A1: G = {A,B,C,D} and

A2: A <> B and

A3: A <> C and

A4: A <> D ; :: thesis: CompF (A,G) = (B '/\' C) '/\' D

for A, B, C, D being a_partition of Y st G = {A,B,C,D} & A <> B & A <> C & A <> D holds

CompF (A,G) = (B '/\' C) '/\' D

let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D being a_partition of Y st G = {A,B,C,D} & A <> B & A <> C & A <> D holds

CompF (A,G) = (B '/\' C) '/\' D

let A, B, C, D be a_partition of Y; :: thesis: ( G = {A,B,C,D} & A <> B & A <> C & A <> D implies CompF (A,G) = (B '/\' C) '/\' D )

assume that

A1: G = {A,B,C,D} and

A2: A <> B and

A3: A <> C and

A4: A <> D ; :: thesis: CompF (A,G) = (B '/\' C) '/\' D

per cases
( B = C or B = D or C = D or ( B <> C & B <> D & C <> D ) )
;

end;

suppose A5:
B = C
; :: thesis: CompF (A,G) = (B '/\' C) '/\' D

then G =
{B,B,A,D}
by A1, ENUMSET1:71

.= {B,A,D} by ENUMSET1:31

.= {A,B,D} by ENUMSET1:58 ;

hence CompF (A,G) = B '/\' D by A2, A4, Th4

.= (B '/\' C) '/\' D by A5, PARTIT1:13 ;

:: thesis: verum

end;.= {B,A,D} by ENUMSET1:31

.= {A,B,D} by ENUMSET1:58 ;

hence CompF (A,G) = B '/\' D by A2, A4, Th4

.= (B '/\' C) '/\' D by A5, PARTIT1:13 ;

:: thesis: verum

suppose A6:
B = D
; :: thesis: CompF (A,G) = (B '/\' C) '/\' D

then G =
{B,B,A,C}
by A1, ENUMSET1:69

.= {B,A,C} by ENUMSET1:31

.= {A,B,C} by ENUMSET1:58 ;

hence CompF (A,G) = B '/\' C by A2, A3, Th4

.= (B '/\' D) '/\' C by A6, PARTIT1:13

.= (B '/\' C) '/\' D by PARTIT1:14 ;

:: thesis: verum

end;.= {B,A,C} by ENUMSET1:31

.= {A,B,C} by ENUMSET1:58 ;

hence CompF (A,G) = B '/\' C by A2, A3, Th4

.= (B '/\' D) '/\' C by A6, PARTIT1:13

.= (B '/\' C) '/\' D by PARTIT1:14 ;

:: thesis: verum

suppose A7:
C = D
; :: thesis: CompF (A,G) = (B '/\' C) '/\' D

then G =
{C,C,A,B}
by A1, ENUMSET1:73

.= {C,A,B} by ENUMSET1:31

.= {A,B,C} by ENUMSET1:59 ;

hence CompF (A,G) = B '/\' C by A2, A3, Th4

.= B '/\' (C '/\' D) by A7, PARTIT1:13

.= (B '/\' C) '/\' D by PARTIT1:14 ;

:: thesis: verum

end;.= {C,A,B} by ENUMSET1:31

.= {A,B,C} by ENUMSET1:59 ;

hence CompF (A,G) = B '/\' C by A2, A3, Th4

.= B '/\' (C '/\' D) by A7, PARTIT1:13

.= (B '/\' C) '/\' D by PARTIT1:14 ;

:: thesis: verum

suppose A8:
( B <> C & B <> D & C <> D )
; :: thesis: CompF (A,G) = (B '/\' C) '/\' D

G \ {A} = ({A} \/ {B,C,D}) \ {A}
by A1, ENUMSET1:4;

then A9: G \ {A} = ({A} \ {A}) \/ ({B,C,D} \ {A}) by XBOOLE_1:42;

A10: not B in {A} by A2, TARSKI:def 1;

A11: ( not C in {A} & not D in {A} ) by A3, A4, TARSKI:def 1;

{B,C,D} \ {A} = ({B} \/ {C,D}) \ {A} by ENUMSET1:2

.= ({B} \ {A}) \/ ({C,D} \ {A}) by XBOOLE_1:42

.= ({B} \ {A}) \/ {C,D} by A11, ZFMISC_1:63

.= {B} \/ {C,D} by A10, ZFMISC_1:59

.= {B,C,D} by ENUMSET1:2 ;

then A12: G \ {A} = {} \/ {B,C,D} by A9, XBOOLE_1:37

.= {B,C,D} ;

A13: (B '/\' C) '/\' D c= '/\' (G \ {A})

hence CompF (A,G) = (B '/\' C) '/\' D by BVFUNC_2:def 7; :: thesis: verum

end;then A9: G \ {A} = ({A} \ {A}) \/ ({B,C,D} \ {A}) by XBOOLE_1:42;

A10: not B in {A} by A2, TARSKI:def 1;

A11: ( not C in {A} & not D in {A} ) by A3, A4, TARSKI:def 1;

{B,C,D} \ {A} = ({B} \/ {C,D}) \ {A} by ENUMSET1:2

.= ({B} \ {A}) \/ ({C,D} \ {A}) by XBOOLE_1:42

.= ({B} \ {A}) \/ {C,D} by A11, ZFMISC_1:63

.= {B} \/ {C,D} by A10, ZFMISC_1:59

.= {B,C,D} by ENUMSET1:2 ;

then A12: G \ {A} = {} \/ {B,C,D} by A9, XBOOLE_1:37

.= {B,C,D} ;

A13: (B '/\' C) '/\' D c= '/\' (G \ {A})

proof

'/\' (G \ {A}) c= (B '/\' C) '/\' D
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (B '/\' C) '/\' D or x in '/\' (G \ {A}) )

reconsider xx = x as set by TARSKI:1;

assume A14: x in (B '/\' C) '/\' D ; :: thesis: x in '/\' (G \ {A})

then A15: x <> {} by EQREL_1:def 4;

x in (INTERSECTION ((B '/\' C),D)) \ {{}} by A14, PARTIT1:def 4;

then consider a, d being set such that

A16: a in B '/\' C and

A17: d in D and

A18: x = a /\ d by SETFAM_1:def 5;

a in (INTERSECTION (B,C)) \ {{}} by A16, PARTIT1:def 4;

then consider b, c being set such that

A19: b in B and

A20: c in C and

A21: a = b /\ c by SETFAM_1:def 5;

set h = (B,C,D) --> (b,c,d);

A22: ((B,C,D) --> (b,c,d)) . D = d by FUNCT_7:94;

A23: ((B,C,D) --> (b,c,d)) . C = c by A8, Lm1;

A24: rng ((B,C,D) --> (b,c,d)) = {(((B,C,D) --> (b,c,d)) . B),(((B,C,D) --> (b,c,d)) . C),(((B,C,D) --> (b,c,d)) . D)} by Lm2

.= {(((B,C,D) --> (b,c,d)) . D),(((B,C,D) --> (b,c,d)) . B),(((B,C,D) --> (b,c,d)) . C)} by ENUMSET1:59 ;

A25: ((B,C,D) --> (b,c,d)) . B = b by A8, FUNCT_4:134;

rng ((B,C,D) --> (b,c,d)) c= bool Y

A27: xx c= Intersect F

((B,C,D) --> (b,c,d)) . p in p

then D in dom ((B,C,D) --> (b,c,d)) by ENUMSET1:def 1;

then A35: rng ((B,C,D) --> (b,c,d)) <> {} by FUNCT_1:3;

Intersect F c= xx

hence x in '/\' (G \ {A}) by A12, A34, A32, A15, BVFUNC_2:def 1; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume A14: x in (B '/\' C) '/\' D ; :: thesis: x in '/\' (G \ {A})

then A15: x <> {} by EQREL_1:def 4;

x in (INTERSECTION ((B '/\' C),D)) \ {{}} by A14, PARTIT1:def 4;

then consider a, d being set such that

A16: a in B '/\' C and

A17: d in D and

A18: x = a /\ d by SETFAM_1:def 5;

a in (INTERSECTION (B,C)) \ {{}} by A16, PARTIT1:def 4;

then consider b, c being set such that

A19: b in B and

A20: c in C and

A21: a = b /\ c by SETFAM_1:def 5;

set h = (B,C,D) --> (b,c,d);

A22: ((B,C,D) --> (b,c,d)) . D = d by FUNCT_7:94;

A23: ((B,C,D) --> (b,c,d)) . C = c by A8, Lm1;

A24: rng ((B,C,D) --> (b,c,d)) = {(((B,C,D) --> (b,c,d)) . B),(((B,C,D) --> (b,c,d)) . C),(((B,C,D) --> (b,c,d)) . D)} by Lm2

.= {(((B,C,D) --> (b,c,d)) . D),(((B,C,D) --> (b,c,d)) . B),(((B,C,D) --> (b,c,d)) . C)} by ENUMSET1:59 ;

A25: ((B,C,D) --> (b,c,d)) . B = b by A8, FUNCT_4:134;

rng ((B,C,D) --> (b,c,d)) c= bool Y

proof

then reconsider F = rng ((B,C,D) --> (b,c,d)) as Subset-Family of Y ;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng ((B,C,D) --> (b,c,d)) or t in bool Y )

assume A26: t in rng ((B,C,D) --> (b,c,d)) ; :: thesis: t in bool Y

end;assume A26: t in rng ((B,C,D) --> (b,c,d)) ; :: thesis: t in bool Y

now :: thesis: ( ( t = ((B,C,D) --> (b,c,d)) . D & t in bool Y ) or ( t = ((B,C,D) --> (b,c,d)) . B & t in bool Y ) or ( t = ((B,C,D) --> (b,c,d)) . C & t in bool Y ) )

hence
t in bool Y
; :: thesis: verumend;

A27: xx c= Intersect F

proof

A32:
for p being set st p in G \ {A} holds
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in xx or u in Intersect F )

assume A28: u in xx ; :: thesis: u in Intersect F

for y being set st y in F holds

u in y

hence u in Intersect F by A24, SETFAM_1:def 9; :: thesis: verum

end;assume A28: u in xx ; :: thesis: u in Intersect F

for y being set st y in F holds

u in y

proof

then
u in meet F
by A24, SETFAM_1:def 1;
let y be set ; :: thesis: ( y in F implies u in y )

assume A29: y in F ; :: thesis: u in y

end;assume A29: y in F ; :: thesis: u in y

now :: thesis: ( ( y = ((B,C,D) --> (b,c,d)) . D & u in y ) or ( y = ((B,C,D) --> (b,c,d)) . B & u in y ) or ( y = ((B,C,D) --> (b,c,d)) . C & u in y ) )end;

hence
u in y
; :: thesis: verumper cases
( y = ((B,C,D) --> (b,c,d)) . D or y = ((B,C,D) --> (b,c,d)) . B or y = ((B,C,D) --> (b,c,d)) . C )
by A24, A29, ENUMSET1:def 1;

end;

hence u in Intersect F by A24, SETFAM_1:def 9; :: thesis: verum

((B,C,D) --> (b,c,d)) . p in p

proof

A34:
dom ((B,C,D) --> (b,c,d)) = {B,C,D}
by FUNCT_4:128;
let p be set ; :: thesis: ( p in G \ {A} implies ((B,C,D) --> (b,c,d)) . p in p )

assume A33: p in G \ {A} ; :: thesis: ((B,C,D) --> (b,c,d)) . p in p

end;assume A33: p in G \ {A} ; :: thesis: ((B,C,D) --> (b,c,d)) . p in p

now :: thesis: ( ( p = D & ((B,C,D) --> (b,c,d)) . p in p ) or ( p = B & ((B,C,D) --> (b,c,d)) . p in p ) or ( p = C & ((B,C,D) --> (b,c,d)) . p in p ) )

hence
((B,C,D) --> (b,c,d)) . p in p
; :: thesis: verumend;

then D in dom ((B,C,D) --> (b,c,d)) by ENUMSET1:def 1;

then A35: rng ((B,C,D) --> (b,c,d)) <> {} by FUNCT_1:3;

Intersect F c= xx

proof

then
x = Intersect F
by A27, XBOOLE_0:def 10;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Intersect F or t in xx )

assume t in Intersect F ; :: thesis: t in xx

then A36: t in meet (rng ((B,C,D) --> (b,c,d))) by A35, SETFAM_1:def 9;

((B,C,D) --> (b,c,d)) . D in rng ((B,C,D) --> (b,c,d)) by A24, ENUMSET1:def 1;

then A37: t in ((B,C,D) --> (b,c,d)) . D by A36, SETFAM_1:def 1;

((B,C,D) --> (b,c,d)) . C in rng ((B,C,D) --> (b,c,d)) by A24, ENUMSET1:def 1;

then A38: t in ((B,C,D) --> (b,c,d)) . C by A36, SETFAM_1:def 1;

((B,C,D) --> (b,c,d)) . B in rng ((B,C,D) --> (b,c,d)) by A24, ENUMSET1:def 1;

then t in ((B,C,D) --> (b,c,d)) . B by A36, SETFAM_1:def 1;

then t in b /\ c by A25, A23, A38, XBOOLE_0:def 4;

hence t in xx by A18, A21, A22, A37, XBOOLE_0:def 4; :: thesis: verum

end;assume t in Intersect F ; :: thesis: t in xx

then A36: t in meet (rng ((B,C,D) --> (b,c,d))) by A35, SETFAM_1:def 9;

((B,C,D) --> (b,c,d)) . D in rng ((B,C,D) --> (b,c,d)) by A24, ENUMSET1:def 1;

then A37: t in ((B,C,D) --> (b,c,d)) . D by A36, SETFAM_1:def 1;

((B,C,D) --> (b,c,d)) . C in rng ((B,C,D) --> (b,c,d)) by A24, ENUMSET1:def 1;

then A38: t in ((B,C,D) --> (b,c,d)) . C by A36, SETFAM_1:def 1;

((B,C,D) --> (b,c,d)) . B in rng ((B,C,D) --> (b,c,d)) by A24, ENUMSET1:def 1;

then t in ((B,C,D) --> (b,c,d)) . B by A36, SETFAM_1:def 1;

then t in b /\ c by A25, A23, A38, XBOOLE_0:def 4;

hence t in xx by A18, A21, A22, A37, XBOOLE_0:def 4; :: thesis: verum

hence x in '/\' (G \ {A}) by A12, A34, A32, A15, BVFUNC_2:def 1; :: thesis: verum

proof

then
'/\' (G \ {A}) = (B '/\' C) '/\' D
by A13, XBOOLE_0:def 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in (B '/\' C) '/\' D )

reconsider xx = x as set by TARSKI:1;

assume x in '/\' (G \ {A}) ; :: thesis: x in (B '/\' C) '/\' D

then consider h being Function, F being Subset-Family of Y such that

A39: dom h = G \ {A} and

A40: rng h = F and

A41: for d being set st d in G \ {A} holds

h . d in d and

A42: x = Intersect F and

A43: x <> {} by BVFUNC_2:def 1;

D in dom h by A12, A39, ENUMSET1:def 1;

then A44: h . D in rng h by FUNCT_1:def 3;

set m = (h . B) /\ (h . C);

B in dom h by A12, A39, ENUMSET1:def 1;

then A45: h . B in rng h by FUNCT_1:def 3;

C in dom h by A12, A39, ENUMSET1:def 1;

then A46: h . C in rng h by FUNCT_1:def 3;

A47: xx c= ((h . B) /\ (h . C)) /\ (h . D)

then A50: not (h . B) /\ (h . C) in {{}} by TARSKI:def 1;

D in G \ {A} by A12, ENUMSET1:def 1;

then A51: h . D in D by A41;

A52: not x in {{}} by A43, TARSKI:def 1;

C in G \ {A} by A12, ENUMSET1:def 1;

then A53: h . C in C by A41;

B in G \ {A} by A12, ENUMSET1:def 1;

then h . B in B by A41;

then (h . B) /\ (h . C) in INTERSECTION (B,C) by A53, SETFAM_1:def 5;

then (h . B) /\ (h . C) in (INTERSECTION (B,C)) \ {{}} by A50, XBOOLE_0:def 5;

then A54: (h . B) /\ (h . C) in B '/\' C by PARTIT1:def 4;

((h . B) /\ (h . C)) /\ (h . D) c= xx

then x in INTERSECTION ((B '/\' C),D) by A51, A54, SETFAM_1:def 5;

then x in (INTERSECTION ((B '/\' C),D)) \ {{}} by A52, XBOOLE_0:def 5;

hence x in (B '/\' C) '/\' D by PARTIT1:def 4; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume x in '/\' (G \ {A}) ; :: thesis: x in (B '/\' C) '/\' D

then consider h being Function, F being Subset-Family of Y such that

A39: dom h = G \ {A} and

A40: rng h = F and

A41: for d being set st d in G \ {A} holds

h . d in d and

A42: x = Intersect F and

A43: x <> {} by BVFUNC_2:def 1;

D in dom h by A12, A39, ENUMSET1:def 1;

then A44: h . D in rng h by FUNCT_1:def 3;

set m = (h . B) /\ (h . C);

B in dom h by A12, A39, ENUMSET1:def 1;

then A45: h . B in rng h by FUNCT_1:def 3;

C in dom h by A12, A39, ENUMSET1:def 1;

then A46: h . C in rng h by FUNCT_1:def 3;

A47: xx c= ((h . B) /\ (h . C)) /\ (h . D)

proof

then
(h . B) /\ (h . C) <> {}
by A43;
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in xx or m in ((h . B) /\ (h . C)) /\ (h . D) )

assume m in xx ; :: thesis: m in ((h . B) /\ (h . C)) /\ (h . D)

then A48: m in meet (rng h) by A40, A42, A45, SETFAM_1:def 9;

then ( m in h . B & m in h . C ) by A45, A46, SETFAM_1:def 1;

then A49: m in (h . B) /\ (h . C) by XBOOLE_0:def 4;

m in h . D by A44, A48, SETFAM_1:def 1;

hence m in ((h . B) /\ (h . C)) /\ (h . D) by A49, XBOOLE_0:def 4; :: thesis: verum

end;assume m in xx ; :: thesis: m in ((h . B) /\ (h . C)) /\ (h . D)

then A48: m in meet (rng h) by A40, A42, A45, SETFAM_1:def 9;

then ( m in h . B & m in h . C ) by A45, A46, SETFAM_1:def 1;

then A49: m in (h . B) /\ (h . C) by XBOOLE_0:def 4;

m in h . D by A44, A48, SETFAM_1:def 1;

hence m in ((h . B) /\ (h . C)) /\ (h . D) by A49, XBOOLE_0:def 4; :: thesis: verum

then A50: not (h . B) /\ (h . C) in {{}} by TARSKI:def 1;

D in G \ {A} by A12, ENUMSET1:def 1;

then A51: h . D in D by A41;

A52: not x in {{}} by A43, TARSKI:def 1;

C in G \ {A} by A12, ENUMSET1:def 1;

then A53: h . C in C by A41;

B in G \ {A} by A12, ENUMSET1:def 1;

then h . B in B by A41;

then (h . B) /\ (h . C) in INTERSECTION (B,C) by A53, SETFAM_1:def 5;

then (h . B) /\ (h . C) in (INTERSECTION (B,C)) \ {{}} by A50, XBOOLE_0:def 5;

then A54: (h . B) /\ (h . C) in B '/\' C by PARTIT1:def 4;

((h . B) /\ (h . C)) /\ (h . D) c= xx

proof

then
((h . B) /\ (h . C)) /\ (h . D) = x
by A47, XBOOLE_0:def 10;
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in ((h . B) /\ (h . C)) /\ (h . D) or m in xx )

assume A55: m in ((h . B) /\ (h . C)) /\ (h . D) ; :: thesis: m in xx

then A56: m in (h . B) /\ (h . C) by XBOOLE_0:def 4;

A57: rng h c= {(h . B),(h . C),(h . D)}

m in y

hence m in xx by A40, A42, A45, SETFAM_1:def 9; :: thesis: verum

end;assume A55: m in ((h . B) /\ (h . C)) /\ (h . D) ; :: thesis: m in xx

then A56: m in (h . B) /\ (h . C) by XBOOLE_0:def 4;

A57: rng h c= {(h . B),(h . C),(h . D)}

proof

for y being set st y in rng h holds
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng h or u in {(h . B),(h . C),(h . D)} )

assume u in rng h ; :: thesis: u in {(h . B),(h . C),(h . D)}

then consider x1 being object such that

A58: x1 in dom h and

A59: u = h . x1 by FUNCT_1:def 3;

end;assume u in rng h ; :: thesis: u in {(h . B),(h . C),(h . D)}

then consider x1 being object such that

A58: x1 in dom h and

A59: u = h . x1 by FUNCT_1:def 3;

now :: thesis: ( ( x1 = B & u in {(h . B),(h . C),(h . D)} ) or ( x1 = C & u in {(h . B),(h . C),(h . D)} ) or ( x1 = D & u in {(h . B),(h . C),(h . D)} ) )

hence
u in {(h . B),(h . C),(h . D)}
; :: thesis: verumend;

m in y

proof

then
m in meet (rng h)
by A45, SETFAM_1:def 1;
let y be set ; :: thesis: ( y in rng h implies m in y )

assume A60: y in rng h ; :: thesis: m in y

end;assume A60: y in rng h ; :: thesis: m in y

now :: thesis: ( ( y = h . B & m in y ) or ( y = h . C & m in y ) or ( y = h . D & m in y ) )end;

hence
m in y
; :: thesis: verumhence m in xx by A40, A42, A45, SETFAM_1:def 9; :: thesis: verum

then x in INTERSECTION ((B '/\' C),D) by A51, A54, SETFAM_1:def 5;

then x in (INTERSECTION ((B '/\' C),D)) \ {{}} by A52, XBOOLE_0:def 5;

hence x in (B '/\' C) '/\' D by PARTIT1:def 4; :: thesis: verum

hence CompF (A,G) = (B '/\' C) '/\' D by BVFUNC_2:def 7; :: thesis: verum