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 A1: ( G = {B,C,D} & B <> C & C <> D & D <> B ) ; :: thesis: '/\' G = (B '/\' C) '/\' D
A2: (B '/\' C) '/\' D c= '/\' G
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (B '/\' C) '/\' D or x in '/\' G )
assume A3: x in (B '/\' C) '/\' D ; :: thesis: x in '/\' G
then x in (INTERSECTION (B '/\' C),D) \ {{} } by PARTIT1:def 4;
then consider a, d being set such that
A4: ( a in B '/\' C & d in D & x = a /\ d ) by SETFAM_1:def 5;
a in (INTERSECTION B,C) \ {{} } by A4, PARTIT1:def 4;
then consider b, c being set such that
A5: ( b in B & c in C & a = b /\ c ) by SETFAM_1:def 5;
set h = ((B .--> b) +* (C .--> c)) +* (D .--> d);
A6: dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = {B,C,D} by Lm1;
A7: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D = d by FUNCT_7:96;
A8: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = b by A1, Lm3;
A9: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C = c by A1, Lm2;
A10: for p being set st p in G holds
(((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p
proof
let p be set ; :: thesis: ( p in G implies (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p )
assume A11: p in G ; :: thesis: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p
now
per cases ( p = D or p = B or p = C ) by A1, A11, ENUMSET1:def 1;
case p = D ; :: thesis: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p
hence (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p by A4, FUNCT_7:96; :: thesis: verum
end;
case p = B ; :: thesis: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p
hence (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p by A1, A5, Lm3; :: thesis: verum
end;
case p = C ; :: thesis: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p
hence (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p by A1, A5, Lm2; :: thesis: verum
end;
end;
end;
hence (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p ; :: thesis: verum
end;
A12: D in dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) by A6, ENUMSET1:def 1;
A13: rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) = {((((B .--> b) +* (C .--> c)) +* (D .--> d)) . B),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . C),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . D)} by Lm4
.= {((((B .--> b) +* (C .--> c)) +* (D .--> d)) . D),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . B),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . C)} by ENUMSET1:100 ;
rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) c= bool Y
proof
let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) or t in bool Y )
assume A14: t in rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) ; :: thesis: t in bool Y
now
per cases ( t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D or t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B or t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C ) by A13, A14, ENUMSET1:def 1;
case t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D ; :: thesis: t in bool Y
hence t in bool Y by A4, A7; :: thesis: verum
end;
case t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B ; :: thesis: t in bool Y
then t = b by A1, Lm3;
hence t in bool Y by A5; :: thesis: verum
end;
case t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C ; :: thesis: t in bool Y
then t = c by A1, Lm2;
hence t in bool Y by A5; :: thesis: verum
end;
end;
end;
hence t in bool Y ; :: thesis: verum
end;
then reconsider F = rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) as Subset-Family of Y ;
A15: rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) <> {} by A12, FUNCT_1:12;
A16: x c= Intersect F
proof
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in x or u in Intersect F )
assume A17: u in x ; :: 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 A18: y in F ; :: thesis: u in y
now
per cases ( y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D or y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B or y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C ) by A13, A18, ENUMSET1:def 1;
case y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D ; :: thesis: u in y
hence u in y by A4, A7, A17, XBOOLE_0:def 4; :: thesis: verum
end;
case A19: y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B ; :: thesis: u in y
u in b /\ (c /\ d) by A4, A5, A17, XBOOLE_1:16;
hence u in y by A8, A19, XBOOLE_0:def 4; :: thesis: verum
end;
case A20: y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C ; :: thesis: u in y
u in c /\ (b /\ d) by A4, A5, A17, XBOOLE_1:16;
hence u in y by A9, A20, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence u in y ; :: thesis: verum
end;
then u in meet F by A13, SETFAM_1:def 1;
hence u in Intersect F by A13, SETFAM_1:def 10; :: thesis: verum
end;
Intersect F c= x
proof
let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in Intersect F or t in x )
assume t in Intersect F ; :: thesis: t in x
then A21: t in meet (rng (((B .--> b) +* (C .--> c)) +* (D .--> d))) by A15, SETFAM_1:def 10;
( (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B in {((((B .--> b) +* (C .--> c)) +* (D .--> d)) . D),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . B),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . C)} & (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C in {((((B .--> b) +* (C .--> c)) +* (D .--> d)) . D),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . B),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . C)} & (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D in {((((B .--> b) +* (C .--> c)) +* (D .--> d)) . D),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . B),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . C)} ) by ENUMSET1:def 1;
then A22: ( t in (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B & t in (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C & t in (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D ) by A13, A21, SETFAM_1:def 1;
then ( t in b & t in c & t in d ) by A1, Lm2, Lm3, FUNCT_7:96;
then t in b /\ c by XBOOLE_0:def 4;
hence t in x by A4, A5, A7, A22, XBOOLE_0:def 4; :: thesis: verum
end;
then A23: x = Intersect F by A16, XBOOLE_0:def 10;
x <> {} by A3, EQREL_1:def 6;
hence x in '/\' G by A1, A6, A10, A23, BVFUNC_2:def 1; :: thesis: verum
end;
'/\' G c= (B '/\' C) '/\' D
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' G or x in (B '/\' C) '/\' D )
assume x in '/\' G ; :: thesis: x in (B '/\' C) '/\' D
then consider h being Function, F being Subset-Family of Y such that
A24: ( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) by BVFUNC_2:def 1;
( B in G & C in G & D in G ) by A1, ENUMSET1:def 1;
then A25: ( h . B in B & h . C in C & h . D in D ) by A24;
( B in dom h & C in dom h & D in dom h ) by A1, A24, ENUMSET1:def 1;
then A26: ( h . B in rng h & h . C in rng h & h . D in rng h ) by FUNCT_1:def 5;
A27: not x in {{} } by A24, TARSKI:def 1;
A28: ((h . B) /\ (h . C)) /\ (h . D) c= x
proof
let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in ((h . B) /\ (h . C)) /\ (h . D) or m in x )
assume A29: m in ((h . B) /\ (h . C)) /\ (h . D) ; :: thesis: m in x
then A30: ( m in (h . B) /\ (h . C) & m in h . D ) by XBOOLE_0:def 4;
A31: rng h c= {(h . B),(h . C),(h . D)}
proof
let u be set ; :: 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 set such that
A32: ( x1 in dom h & u = h . x1 ) by FUNCT_1:def 5;
now
per cases ( x1 = B or x1 = C or x1 = D ) by A1, A24, A32, 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 A32, 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 A32, 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 A32, 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 A33: y in rng h ; :: thesis: m in y
now
per cases ( y = h . B or y = h . C or y = h . D ) by A31, A33, ENUMSET1:def 1;
end;
end;
hence m in y ; :: thesis: verum
end;
then m in meet (rng h) by A26, SETFAM_1:def 1;
hence m in x by A24, A26, SETFAM_1:def 10; :: thesis: verum
end;
A34: x c= ((h . B) /\ (h . C)) /\ (h . D)
proof
let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in x or m in ((h . B) /\ (h . C)) /\ (h . D) )
assume m in x ; :: thesis: m in ((h . B) /\ (h . C)) /\ (h . D)
then m in meet (rng h) by A24, A26, SETFAM_1:def 10;
then A35: ( m in h . B & m in h . C & m in h . D ) by A26, SETFAM_1:def 1;
then m in (h . B) /\ (h . C) by XBOOLE_0:def 4;
hence m in ((h . B) /\ (h . C)) /\ (h . D) by A35, XBOOLE_0:def 4; :: thesis: verum
end;
then A36: ((h . B) /\ (h . C)) /\ (h . D) = x by A28, XBOOLE_0:def 10;
set m = (h . B) /\ (h . C);
(h . B) /\ (h . C) <> {} by A24, A34;
then A37: not (h . B) /\ (h . C) in {{} } by TARSKI:def 1;
(h . B) /\ (h . C) in INTERSECTION B,C by A25, SETFAM_1:def 5;
then (h . B) /\ (h . C) in (INTERSECTION B,C) \ {{} } by A37, XBOOLE_0:def 5;
then (h . B) /\ (h . C) in B '/\' C by PARTIT1:def 4;
then x in INTERSECTION (B '/\' C),D by A25, A36, SETFAM_1:def 5;
then x in (INTERSECTION (B '/\' C),D) \ {{} } by A27, XBOOLE_0:def 5;
hence x in (B '/\' C) '/\' D by PARTIT1:def 4; :: thesis: verum
end;
hence '/\' G = (B '/\' C) '/\' D by A2, XBOOLE_0:def 10; :: thesis: verum