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

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

'/\' G = (B '/\' C) '/\' D

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

'/\' G = (B '/\' C) '/\' D

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

assume that

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

A2: B <> C and

A3: C <> D and

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

A5: (B '/\' C) '/\' D c= '/\' G

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

'/\' G = (B '/\' C) '/\' D

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

'/\' G = (B '/\' C) '/\' D

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

assume that

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

A2: B <> C and

A3: C <> D and

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

A5: (B '/\' C) '/\' D c= '/\' G

proof

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

reconsider xx = x as set by TARSKI:1;

assume A6: x in (B '/\' C) '/\' D ; :: thesis: x in '/\' G

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

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

then consider a, d being set such that

A8: a in B '/\' C and

A9: d in D and

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

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

then consider b, c being set such that

A11: b in B and

A12: c in C and

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

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

A14: 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 ;

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

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

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

A18: for p being set st p in G holds

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

A21: xx c= Intersect F

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

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

Intersect F c= xx

hence x in '/\' G by A1, A26, A18, A7, BVFUNC_2:def 1; :: thesis: verum

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

assume A6: x in (B '/\' C) '/\' D ; :: thesis: x in '/\' G

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

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

then consider a, d being set such that

A8: a in B '/\' C and

A9: d in D and

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

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

then consider b, c being set such that

A11: b in B and

A12: c in C and

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

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

A14: 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 ;

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

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 A16: t in rng ((B,C,D) --> (b,c,d)) ; :: thesis: t in bool Y

end;assume A16: 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;

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

A18: for p being set st p in G holds

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

proof

A20:
((B,C,D) --> (b,c,d)) . B = b
by A2, A4, FUNCT_4:134;
let p be set ; :: thesis: ( p in G implies ((B,C,D) --> (b,c,d)) . p in p )

assume A19: p in G ; :: thesis: ((B,C,D) --> (b,c,d)) . p in p

end;assume A19: p in G ; :: 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;

A21: xx c= Intersect F

proof

A26:
dom ((B,C,D) --> (b,c,d)) = {B,C,D}
by FUNCT_4:128;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in xx or u in Intersect F )

assume A22: 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 A14, SETFAM_1:def 9; :: thesis: verum

end;assume A22: 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 A14, SETFAM_1:def 1;
let y be set ; :: thesis: ( y in F implies u in y )

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

end;assume A23: 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 A14, A23, ENUMSET1:def 1;

end;

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

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

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

Intersect F c= xx

proof

then
x = Intersect F
by A21, 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 A28: t in meet (rng ((B,C,D) --> (b,c,d))) by A27, SETFAM_1:def 9;

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

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

then A29: t in c by A3, Lm1;

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

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

then t in b by A2, A4, FUNCT_4:134;

then A30: t in b /\ c by A29, XBOOLE_0:def 4;

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

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

hence t in xx by A10, A13, A15, A30, XBOOLE_0:def 4; :: thesis: verum

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

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

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

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

then A29: t in c by A3, Lm1;

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

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

then t in b by A2, A4, FUNCT_4:134;

then A30: t in b /\ c by A29, XBOOLE_0:def 4;

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

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

hence t in xx by A10, A13, A15, A30, XBOOLE_0:def 4; :: thesis: verum

hence x in '/\' G by A1, A26, A18, A7, BVFUNC_2:def 1; :: thesis: verum

proof

hence
'/\' G = (B '/\' C) '/\' D
by A5, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' G or x in (B '/\' C) '/\' D )

reconsider xx = x as set by TARSKI:1;

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

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

A31: dom h = G and

A32: rng h = F and

A33: for d being set st d in G holds

h . d in d and

A34: x = Intersect F and

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

D in dom h by A1, A31, ENUMSET1:def 1;

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

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

B in dom h by A1, A31, ENUMSET1:def 1;

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

C in dom h by A1, A31, ENUMSET1:def 1;

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

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

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

D in G by A1, ENUMSET1:def 1;

then A43: h . D in D by A33;

A44: not x in {{}} by A35, TARSKI:def 1;

C in G by A1, ENUMSET1:def 1;

then A45: h . C in C by A33;

B in G by A1, ENUMSET1:def 1;

then h . B in B by A33;

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

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

then A46: (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 A43, A46, SETFAM_1:def 5;

then x in (INTERSECTION ((B '/\' C),D)) \ {{}} by A44, 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 ; :: thesis: x in (B '/\' C) '/\' D

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

A31: dom h = G and

A32: rng h = F and

A33: for d being set st d in G holds

h . d in d and

A34: x = Intersect F and

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

D in dom h by A1, A31, ENUMSET1:def 1;

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

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

B in dom h by A1, A31, ENUMSET1:def 1;

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

C in dom h by A1, A31, ENUMSET1:def 1;

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

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

proof

then
(h . B) /\ (h . C) <> {}
by A35;
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 A40: m in meet (rng h) by A32, A34, A37, SETFAM_1:def 9;

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

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

m in h . D by A36, A40, SETFAM_1:def 1;

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

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

then A40: m in meet (rng h) by A32, A34, A37, SETFAM_1:def 9;

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

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

m in h . D by A36, A40, SETFAM_1:def 1;

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

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

D in G by A1, ENUMSET1:def 1;

then A43: h . D in D by A33;

A44: not x in {{}} by A35, TARSKI:def 1;

C in G by A1, ENUMSET1:def 1;

then A45: h . C in C by A33;

B in G by A1, ENUMSET1:def 1;

then h . B in B by A33;

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

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

then A46: (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 A39, 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 A47: m in ((h . B) /\ (h . C)) /\ (h . D) ; :: thesis: m in xx

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

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

m in y

hence m in xx by A32, A34, A37, SETFAM_1:def 9; :: thesis: verum

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

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

A49: 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

A50: x1 in dom h and

A51: 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

A50: x1 in dom h and

A51: 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 A37, SETFAM_1:def 1;
let y be set ; :: thesis: ( y in rng h implies m in y )

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

end;assume A52: 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 A32, A34, A37, SETFAM_1:def 9; :: thesis: verum

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

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

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