let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C being a_partition of Y st G = {A,B,C} & A <> B & C <> A holds
CompF A,G = B '/\' C
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C being a_partition of Y st G = {A,B,C} & A <> B & C <> A holds
CompF A,G = B '/\' C
let A, B, C be a_partition of Y; :: thesis: ( G = {A,B,C} & A <> B & C <> A implies CompF A,G = B '/\' C )
assume that
A1: G = {A,B,C} and
A2: A <> B and
A3: C <> A ; :: thesis: CompF A,G = B '/\' C
per cases ( B = C or B <> C ) ;
suppose A4: B = C ; :: thesis: CompF A,G = B '/\' C
G = {B,C,A} by A1, ENUMSET1:100
.= {B,A} by A4, ENUMSET1:70 ;
hence CompF A,G = B by A2, BVFUNC11:7
.= B '/\' C by A4, PARTIT1:15 ;
:: thesis: verum
end;
suppose A5: B <> C ; :: thesis: CompF A,G = B '/\' C
A6: G \ {A} = ({A} \/ {B,C}) \ {A} by A1, ENUMSET1:42
.= ({A} \ {A}) \/ ({B,C} \ {A}) by XBOOLE_1:42 ;
( not B in {A} & not C in {A} ) by A2, A3, TARSKI:def 1;
then A7: G \ {A} = ({A} \ {A}) \/ {B,C} by A6, ZFMISC_1:72
.= {} \/ {B,C} by XBOOLE_1:37
.= {B,C} ;
A8: '/\' (G \ {A}) c= B '/\' C
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in B '/\' C )
assume x in '/\' (G \ {A}) ; :: thesis: x in B '/\' C
then consider h being Function, F being Subset-Family of Y such that
A9: dom h = G \ {A} and
A10: rng h = F and
A11: for d being set st d in G \ {A} holds
h . d in d and
A12: x = Intersect F and
A13: x <> {} by BVFUNC_2:def 1;
A14: not x in {{} } by A13, TARSKI:def 1;
B in dom h by A7, A9, TARSKI:def 2;
then A15: h . B in rng h by FUNCT_1:def 5;
A16: (h . B) /\ (h . C) c= x
proof
let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in (h . B) /\ (h . C) or m in x )
assume A17: m in (h . B) /\ (h . C) ; :: thesis: m in x
A18: rng h c= {(h . B),(h . C)}
proof
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng h or u in {(h . B),(h . C)} )
assume u in rng h ; :: thesis: u in {(h . B),(h . C)}
then consider x1 being set such that
A19: x1 in dom h and
A20: u = h . x1 by FUNCT_1:def 5;
now
per cases ( x1 = B or x1 = C ) by A7, A9, A19, TARSKI:def 2;
case x1 = B ; :: thesis: u in {(h . B),(h . C)}
hence u in {(h . B),(h . C)} by A20, TARSKI:def 2; :: thesis: verum
end;
case x1 = C ; :: thesis: u in {(h . B),(h . C)}
hence u in {(h . B),(h . C)} by A20, TARSKI:def 2; :: thesis: verum
end;
end;
end;
hence u in {(h . B),(h . C)} ; :: 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 A21: y in rng h ; :: thesis: m in y
now
per cases ( y = h . B or y = h . C ) by A18, A21, TARSKI:def 2;
end;
end;
hence m in y ; :: thesis: verum
end;
then m in meet (rng h) by A15, SETFAM_1:def 1;
hence m in x by A10, A12, A15, SETFAM_1:def 10; :: thesis: verum
end;
C in G \ {A} by A7, TARSKI:def 2;
then A22: h . C in C by A11;
B in G \ {A} by A7, TARSKI:def 2;
then A23: h . B in B by A11;
C in dom h by A7, A9, TARSKI:def 2;
then A24: h . C in rng h by FUNCT_1:def 5;
x c= (h . B) /\ (h . C)
proof
let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in x or m in (h . B) /\ (h . C) )
assume m in x ; :: thesis: m in (h . B) /\ (h . C)
then m in meet (rng h) by A10, A12, A15, SETFAM_1:def 10;
then ( m in h . B & m in h . C ) by A15, A24, SETFAM_1:def 1;
hence m in (h . B) /\ (h . C) by XBOOLE_0:def 4; :: thesis: verum
end;
then (h . B) /\ (h . C) = x by A16, XBOOLE_0:def 10;
then x in INTERSECTION B,C by A23, A22, SETFAM_1:def 5;
then x in (INTERSECTION B,C) \ {{} } by A14, XBOOLE_0:def 5;
hence x in B '/\' C by PARTIT1:def 4; :: thesis: verum
end;
A25: B '/\' C c= '/\' (G \ {A})
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B '/\' C or x in '/\' (G \ {A}) )
assume A26: x in B '/\' C ; :: thesis: x in '/\' (G \ {A})
then A27: x <> {} by EQREL_1:def 6;
x in (INTERSECTION B,C) \ {{} } by A26, PARTIT1:def 4;
then consider a, b being set such that
A28: a in B and
A29: b in C and
A30: x = a /\ b by SETFAM_1:def 5;
set h0 = B,C --> a,b;
A31: dom (B,C --> a,b) = G \ {A} by A7, FUNCT_4:65;
A32: rng (B,C --> a,b) = {a,b} by A5, FUNCT_4:67;
rng (B,C --> a,b) c= bool Y
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (B,C --> a,b) or y in bool Y )
assume A33: y in rng (B,C --> a,b) ; :: thesis: y in bool Y
now
end;
hence y in bool Y ; :: thesis: verum
end;
then reconsider F = rng (B,C --> a,b) as Subset-Family of Y ;
A34: 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 A35: 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 A36: y in F ; :: thesis: u in y
hence u in y ; :: thesis: verum
end;
then u in meet F by A32, SETFAM_1:def 1;
hence u in Intersect F by A32, SETFAM_1:def 10; :: thesis: verum
end;
A37: for d being set st d in G \ {A} holds
(B,C --> a,b) . d in d
proof
let d be set ; :: thesis: ( d in G \ {A} implies (B,C --> a,b) . d in d )
assume A38: d in G \ {A} ; :: thesis: (B,C --> a,b) . d in d
now
per cases ( d = B or d = C ) by A7, A38, TARSKI:def 2;
case d = B ; :: thesis: (B,C --> a,b) . d in d
hence (B,C --> a,b) . d in d by A5, A28, FUNCT_4:66; :: thesis: verum
end;
case d = C ; :: thesis: (B,C --> a,b) . d in d
hence (B,C --> a,b) . d in d by A29, FUNCT_4:66; :: thesis: verum
end;
end;
end;
hence (B,C --> a,b) . d in d ; :: thesis: verum
end;
Intersect F c= x then x = Intersect F by A34, XBOOLE_0:def 10;
hence x in '/\' (G \ {A}) by A31, A37, A27, BVFUNC_2:def 1; :: thesis: verum
end;
CompF A,G = '/\' (G \ {A}) by BVFUNC_2:def 7;
hence CompF A,G = B '/\' C by A25, A8, XBOOLE_0:def 10; :: thesis: verum
end;
end;