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
proof
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
proof
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
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 ) )
per cases ( t = ((B,C,D) --> (b,c,d)) . D or t = ((B,C,D) --> (b,c,d)) . B or t = ((B,C,D) --> (b,c,d)) . C ) by A14, A16, ENUMSET1:def 1;
case t = ((B,C,D) --> (b,c,d)) . D ; :: thesis: t in bool Y
hence t in bool Y by A9, A15; :: thesis: verum
end;
case t = ((B,C,D) --> (b,c,d)) . B ; :: thesis: t in bool Y
then t = b by A2, A4, FUNCT_4:134;
hence t in bool Y by A11; :: thesis: verum
end;
case t = ((B,C,D) --> (b,c,d)) . C ; :: thesis: t in bool Y
then t = c by A3, Lm1;
hence t in bool Y by A12; :: thesis: verum
end;
end;
end;
hence t in bool Y ; :: thesis: verum
end;
then reconsider F = rng ((B,C,D) --> (b,c,d)) as Subset-Family of 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
proof
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
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 ) )
per cases ( p = D or p = B or p = C ) by A1, A19, ENUMSET1:def 1;
case p = D ; :: thesis: ((B,C,D) --> (b,c,d)) . p in p
hence ((B,C,D) --> (b,c,d)) . p in p by A9, FUNCT_7:94; :: thesis: verum
end;
case p = B ; :: thesis: ((B,C,D) --> (b,c,d)) . p in p
hence ((B,C,D) --> (b,c,d)) . p in p by A2, A4, A11, FUNCT_4:134; :: thesis: verum
end;
case p = C ; :: thesis: ((B,C,D) --> (b,c,d)) . p in p
hence ((B,C,D) --> (b,c,d)) . p in p by A3, A12, Lm1; :: thesis: verum
end;
end;
end;
hence ((B,C,D) --> (b,c,d)) . p in p ; :: thesis: verum
end;
A20: ((B,C,D) --> (b,c,d)) . B = b by A2, A4, FUNCT_4:134;
A21: xx c= Intersect F
proof
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
proof
let y be set ; :: thesis: ( y in F implies u in y )
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 ) )
per 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;
case y = ((B,C,D) --> (b,c,d)) . D ; :: thesis: u in y
hence u in y by A10, A15, A22, XBOOLE_0:def 4; :: thesis: verum
end;
case A24: y = ((B,C,D) --> (b,c,d)) . B ; :: thesis: u in y
u in b /\ (c /\ d) by A10, A13, A22, XBOOLE_1:16;
hence u in y by A20, A24, XBOOLE_0:def 4; :: thesis: verum
end;
case A25: y = ((B,C,D) --> (b,c,d)) . C ; :: thesis: u in y
u in c /\ (b /\ d) by A10, A13, A22, XBOOLE_1:16;
hence u in y by A17, A25, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence u in y ; :: thesis: verum
end;
then u in meet F by A14, SETFAM_1:def 1;
hence u in Intersect F by A14, SETFAM_1:def 9; :: thesis: verum
end;
A26: dom ((B,C,D) --> (b,c,d)) = {B,C,D} by FUNCT_4:128;
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
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;
then x = Intersect F by A21, XBOOLE_0:def 10;
hence x in '/\' G by A1, A26, A18, A7, BVFUNC_2:def 1; :: thesis: verum
end;
'/\' G c= (B '/\' C) '/\' D
proof
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)
proof
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;
then (h . B) /\ (h . C) <> {} by A35;
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
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)}
proof
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;
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)} ) )
per cases ( x1 = B or x1 = C or x1 = D ) by A1, A31, A50, ENUMSET1:def 1;
case x1 = B ; :: thesis: u in {(h . B),(h . C),(h . D)}
hence u in {(h . B),(h . C),(h . D)} by A51, ENUMSET1:def 1; :: thesis: verum
end;
case x1 = C ; :: thesis: u in {(h . B),(h . C),(h . D)}
hence u in {(h . B),(h . C),(h . D)} by A51, ENUMSET1:def 1; :: thesis: verum
end;
case x1 = D ; :: thesis: u in {(h . B),(h . C),(h . D)}
hence u in {(h . B),(h . C),(h . D)} by A51, ENUMSET1:def 1; :: thesis: verum
end;
end;
end;
hence u in {(h . B),(h . C),(h . D)} ; :: thesis: verum
end;
for y being set st y in rng h holds
m in y
proof
let y be set ; :: thesis: ( y in rng h implies m in y )
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 ) )
per cases ( y = h . B or y = h . C or y = h . D ) by A49, A52, ENUMSET1:def 1;
end;
end;
hence m in y ; :: thesis: verum
end;
then m in meet (rng h) by A37, SETFAM_1:def 1;
hence m in xx by A32, A34, A37, SETFAM_1:def 9; :: thesis: verum
end;
then ((h . B) /\ (h . C)) /\ (h . D) = x by A39, XBOOLE_0:def 10;
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;
hence '/\' G = (B '/\' C) '/\' D by A5, XBOOLE_0:def 10; :: thesis: verum