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 st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & EqClass z,(C '/\' D) = EqClass u,(C '/\' D) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
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 st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & EqClass z,(C '/\' D) = EqClass u,(C '/\' D) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let A, B, C, D be a_partition of Y; :: thesis: for z, u being Element of Y st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & EqClass z,(C '/\' D) = EqClass u,(C '/\' D) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let z, u be Element of Y; :: thesis: ( G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & EqClass z,(C '/\' D) = EqClass u,(C '/\' D) implies EqClass u,(CompF A,G) meets EqClass z,(CompF B,G) )
assume A1:
( G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & EqClass z,(C '/\' D) = EqClass u,(C '/\' D) )
; :: thesis: EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
then A2:
CompF B,G = (A '/\' C) '/\' D
by Th8;
set H = EqClass z,(CompF B,G);
set I = EqClass z,A;
set GG = EqClass u,((B '/\' C) '/\' D);
set h = (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A));
A3:
dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) = G
by A1, Th19;
A4:
((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . A = EqClass z,A
by FUNCT_7:96;
A5:
((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . B = EqClass u,B
by A1, Th18;
A6:
((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . C = EqClass u,C
by A1, Th18;
A7:
((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . D = EqClass u,D
by A1, Th18;
A8:
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 A9:
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 A1, A9, ENUMSET1:def 2;
suppose A11:
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 A1, Th18;
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 = 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 A1, Th18;
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 = 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 A1, Th18;
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;
end;
A in dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A)))
by A1, A3, ENUMSET1:def 2;
then A14:
((((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 5;
B in dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A)))
by A1, A3, ENUMSET1:def 2;
then A15:
((((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 5;
C in dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A)))
by A1, A3, ENUMSET1:def 2;
then A16:
((((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 5;
D in dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A)))
by A1, A3, ENUMSET1:def 2;
then A17:
((((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 5;
A18:
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 A1, Th20;
rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) c= bool Y
proof
let t be
set ;
:: 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 A19:
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 A18, A19, ENUMSET1:def 2;
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 ;
( dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) = G & rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) = FF & ( 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 ) )
by A1, A8, Th19;
then
Intersect FF <> {}
by A1, BVFUNC_2:def 5;
then consider m being set such that
A20:
m in Intersect FF
by XBOOLE_0:def 1;
m in meet FF
by A14, A20, SETFAM_1:def 10;
then A21:
( m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . A & m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . B & m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . C & m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . D )
by A14, A15, A16, A17, SETFAM_1:def 1;
A22:
EqClass u,((B '/\' C) '/\' D) = (EqClass u,(B '/\' C)) /\ (EqClass u,D)
by Th1;
m in (EqClass u,B) /\ (EqClass u,C)
by A5, A6, A21, XBOOLE_0:def 4;
then
m in ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)
by A7, A21, XBOOLE_0:def 4;
then
m in (((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass z,A)
by A4, A21, XBOOLE_0:def 4;
then
(EqClass u,((B '/\' C) '/\' D)) /\ (EqClass z,A) <> {}
by A22, Th1;
then consider p being set such that
A23:
p in (EqClass u,((B '/\' C) '/\' D)) /\ (EqClass z,A)
by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A23;
set K = EqClass p,(C '/\' D);
A24:
( p in EqClass p,(C '/\' D) & EqClass p,(C '/\' D) in C '/\' D )
by EQREL_1:def 8;
A25:
( p in EqClass u,((B '/\' C) '/\' D) & p in EqClass z,A )
by A23, XBOOLE_0:def 4;
then
p in (EqClass z,A) /\ (EqClass p,(C '/\' D))
by A24, XBOOLE_0:def 4;
then
( (EqClass z,A) /\ (EqClass p,(C '/\' D)) in INTERSECTION A,(C '/\' D) & not (EqClass z,A) /\ (EqClass p,(C '/\' D)) in {{} } )
by SETFAM_1:def 5, TARSKI:def 1;
then A26:
(EqClass z,A) /\ (EqClass p,(C '/\' D)) in (INTERSECTION A,(C '/\' D)) \ {{} }
by XBOOLE_0:def 5;
set L = EqClass z,(C '/\' D);
EqClass u,((B '/\' C) '/\' D) = EqClass u,(B '/\' (C '/\' D))
by PARTIT1:16;
then A27:
EqClass u,((B '/\' C) '/\' D) c= EqClass u,(C '/\' D)
by BVFUNC11:3;
A28:
p in EqClass u,((B '/\' C) '/\' D)
by A23, XBOOLE_0:def 4;
p in EqClass p,(C '/\' D)
by EQREL_1:def 8;
then
EqClass p,(C '/\' D) meets EqClass z,(C '/\' D)
by A1, A27, A28, XBOOLE_0:3;
then
EqClass p,(C '/\' D) = EqClass z,(C '/\' D)
by EQREL_1:50;
then A29:
z in EqClass p,(C '/\' D)
by EQREL_1:def 8;
z in EqClass z,A
by EQREL_1:def 8;
then A30:
z in (EqClass z,A) /\ (EqClass p,(C '/\' D))
by A29, XBOOLE_0:def 4;
A31:
z in EqClass z,(CompF B,G)
by EQREL_1:def 8;
A '/\' (C '/\' D) = (A '/\' C) '/\' D
by PARTIT1:16;
then
(EqClass z,A) /\ (EqClass p,(C '/\' D)) in CompF B,G
by A2, A26, PARTIT1:def 4;
then
( (EqClass z,A) /\ (EqClass p,(C '/\' D)) = EqClass z,(CompF B,G) or (EqClass z,A) /\ (EqClass p,(C '/\' D)) misses EqClass z,(CompF B,G) )
by EQREL_1:def 6;
then
p in EqClass z,(CompF B,G)
by A24, A25, A30, A31, XBOOLE_0:3, XBOOLE_0:def 4;
then
p in (EqClass u,((B '/\' C) '/\' D)) /\ (EqClass z,(CompF B,G))
by A28, XBOOLE_0:def 4;
then
EqClass u,((B '/\' C) '/\' D) meets EqClass z,(CompF B,G)
by XBOOLE_0:4;
hence
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
by A1, Th7; :: thesis: verum