let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D holds
EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D holds
EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)
let A, B, C, D be a_partition of Y; :: thesis: for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D holds
EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)
let z, u be Element of Y; :: thesis: for h being Function st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D holds
EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)
let h be Function; :: thesis: ( G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D implies EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A) )
assume that
A1: G is independent and
A2: G = {A,B,C,D} and
A3: ( A <> B & A <> C & A <> D & B <> C & B <> D & C <> D ) ; :: thesis: EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)
set h = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)));
A4: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by A3, Th15;
A5: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D) by A3, Th15;
A6: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by A3, Th15;
A7: rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) = {(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . A),(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . B),(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . C),(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . D)} by A2, Th17;
rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) c= bool Y
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) or t in bool Y )
assume A8: t in rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) ; :: thesis: t in bool Y
per cases ( t = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . A or t = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . B or t = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . C or t = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . D ) by A7, A8, ENUMSET1:def 2;
suppose t = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . A ; :: thesis: t in bool Y
then t = EqClass (z,A) by FUNCT_7:94;
hence t in bool Y ; :: thesis: verum
end;
suppose t = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . B ; :: thesis: t in bool Y
hence t in bool Y by A4; :: thesis: verum
end;
suppose t = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . C ; :: thesis: t in bool Y
hence t in bool Y by A6; :: thesis: verum
end;
suppose t = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . D ; :: thesis: t in bool Y
hence t in bool Y by A5; :: thesis: verum
end;
end;
end;
then reconsider FF = rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) as Subset-Family of Y ;
A9: dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) = G by A2, Th16;
for d being set st d in G holds
((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d
proof
let d be set ; :: thesis: ( d in G implies ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d )
assume A10: d in G ; :: thesis: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d
per cases ( d = A or d = B or d = C or d = D ) by A2, A10, ENUMSET1:def 2;
suppose A11: d = A ; :: thesis: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d
((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by FUNCT_7:94;
hence ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d by A11; :: thesis: verum
end;
suppose A12: d = B ; :: thesis: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d
((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by A3, Th15;
hence ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d by A12; :: thesis: verum
end;
suppose A13: d = C ; :: thesis: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d
((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by A3, Th15;
hence ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d by A13; :: thesis: verum
end;
suppose A14: d = D ; :: thesis: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d
((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D) by A3, Th15;
hence ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d by A14; :: thesis: verum
end;
end;
end;
then Intersect FF <> {} by A1, A9, BVFUNC_2:def 5;
then consider m being object such that
A15: m in Intersect FF by XBOOLE_0:def 1;
A in dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by A2, A9, ENUMSET1:def 2;
then A16: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . A in rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A17: m in meet FF by A15, SETFAM_1:def 9;
D in dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by A2, A9, ENUMSET1:def 2;
then ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . D in rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A18: m in ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . D by A17, SETFAM_1:def 1;
C in dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by A2, A9, ENUMSET1:def 2;
then ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . C in rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A19: m in ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . C by A17, SETFAM_1:def 1;
B in dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by A2, A9, ENUMSET1:def 2;
then ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . B in rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . B by A17, SETFAM_1:def 1;
then m in (EqClass (u,B)) /\ (EqClass (u,C)) by A4, A6, A19, XBOOLE_0:def 4;
then A20: m in ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D)) by A5, A18, XBOOLE_0:def 4;
( ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) & m in ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . A ) by A16, A17, FUNCT_7:94, SETFAM_1:def 1;
then m in (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (z,A)) by A20, XBOOLE_0:def 4;
then A21: ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D)) meets EqClass (z,A) by XBOOLE_0:4;
EqClass (u,((B '/\' C) '/\' D)) = (EqClass (u,(B '/\' C))) /\ (EqClass (u,D)) by Th1;
hence EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A) by A21, Th1; :: thesis: verum