let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C} & A <> B & B <> C & C <> A & EqClass (z,C) = EqClass (u,C) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C} & A <> B & B <> C & C <> A & EqClass (z,C) = EqClass (u,C) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
let A, B, C be a_partition of Y; :: thesis: for z, u being Element of Y st G is independent & G = {A,B,C} & A <> B & B <> C & C <> A & EqClass (z,C) = EqClass (u,C) 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} & A <> B & B <> C & C <> A & EqClass (z,C) = EqClass (u,C) implies EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G))) )
assume that
A1: G is independent and
A2: G = {A,B,C} and
A3: A <> B and
A4: B <> C and
A5: C <> A and
A6: EqClass (z,C) = EqClass (u,C) ; :: thesis: EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
set h = ((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)));
A in dom (A .--> (EqClass (z,A))) by TARSKI:def 1;
then (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A = (A .--> (EqClass (z,A))) . A by FUNCT_4:13;
then A8: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by FUNCOP_1:72;
set H = EqClass (z,(CompF (B,G)));
set I = EqClass (z,A);
set GG = EqClass (u,(B '/\' C));
A9: (EqClass (u,(B '/\' C))) /\ (EqClass (z,A)) = ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (z,A)) by Th1;
dom ((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) = (dom (B .--> (EqClass (u,B)))) \/ (dom (C .--> (EqClass (u,C)))) by FUNCT_4:def 1;
then A10: dom (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) = ((dom (B .--> (EqClass (u,B)))) \/ (dom (C .--> (EqClass (u,C))))) \/ (dom (A .--> (EqClass (z,A)))) by FUNCT_4:def 1;
A12: C in dom (C .--> (EqClass (u,C))) by TARSKI:def 1;
not B in dom (A .--> (EqClass (z,A))) by A3, TARSKI:def 1;
then A13: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B = ((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) . B by FUNCT_4:11;
not B in dom (C .--> (EqClass (u,C))) by A4, TARSKI:def 1;
then (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B = (B .--> (EqClass (u,B))) . B by A13, FUNCT_4:11;
then A14: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by FUNCOP_1:72;
not C in dom (A .--> (EqClass (z,A))) by A5, TARSKI:def 1;
then (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C = ((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) . C by FUNCT_4:11;
then (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C = (C .--> (EqClass (u,C))) . C by A12, FUNCT_4:13;
then A15: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by FUNCOP_1:72;
A16: dom (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) = ({A} \/ {B}) \/ {C} by A10, XBOOLE_1:4
.= {A,B} \/ {C} by ENUMSET1:1
.= {A,B,C} by ENUMSET1:3 ;
A17: rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) c= {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)}
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) or t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)} )
assume t in rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) ; :: thesis: t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)}
then consider x1 being object such that
A18: x1 in dom (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) and
A19: t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . x1 by FUNCT_1:def 3;
now :: thesis: ( ( x1 = A & t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)} ) or ( x1 = B & t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)} ) or ( x1 = C & t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)} ) )
per cases ( x1 = A or x1 = B or x1 = C ) by A16, A18, ENUMSET1:def 1;
case x1 = A ; :: thesis: t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)}
hence t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)} by A19, ENUMSET1:def 1; :: thesis: verum
end;
case x1 = B ; :: thesis: t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)}
hence t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)} by A19, ENUMSET1:def 1; :: thesis: verum
end;
case x1 = C ; :: thesis: t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)}
hence t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)} by A19, ENUMSET1:def 1; :: thesis: verum
end;
end;
end;
hence t in {((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B),((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C)} ; :: thesis: verum
end;
rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (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)))) +* (A .--> (EqClass (z,A)))) or t in bool Y )
assume A20: t in rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) ; :: thesis: t in bool Y
now :: thesis: ( ( t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A & t in bool Y ) or ( t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B & t in bool Y ) or ( t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C & t in bool Y ) )
per cases ( t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A or t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B or t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C ) by A17, A20, ENUMSET1:def 1;
case t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A ; :: thesis: t in bool Y
hence t in bool Y by A8; :: thesis: verum
end;
case t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B ; :: thesis: t in bool Y
hence t in bool Y by A14; :: thesis: verum
end;
case t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C ; :: thesis: t in bool Y
hence t in bool Y by A15; :: thesis: verum
end;
end;
end;
hence t in bool Y ; :: thesis: verum
end;
then reconsider FF = rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) as Subset-Family of Y ;
A21: z in EqClass (z,(CompF (B,G))) by EQREL_1:def 6;
for d being set st d in G holds
(((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (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)))) +* (A .--> (EqClass (z,A)))) . d in d )
assume A22: d in G ; :: thesis: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d
now :: thesis: ( ( d = A & (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = B & (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = C & (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d ) )
per cases ( d = A or d = B or d = C ) by A2, A22, ENUMSET1:def 1;
case d = A ; :: thesis: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d
hence (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d by A8; :: thesis: verum
end;
case d = B ; :: thesis: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d
hence (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d by A14; :: thesis: verum
end;
case d = C ; :: thesis: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d
hence (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d by A15; :: thesis: verum
end;
end;
end;
hence (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d ; :: thesis: verum
end;
then Intersect FF <> {} by A1, A2, A16, BVFUNC_2:def 5;
then consider m being object such that
A23: m in Intersect FF by XBOOLE_0:def 1;
A in dom (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) by A16, ENUMSET1:def 1;
then A24: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A in rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A25: Intersect FF = meet (rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A))))) by SETFAM_1:def 9;
C in dom (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) by A16, ENUMSET1:def 1;
then (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C in rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A26: m in (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C by A25, A23, SETFAM_1:def 1;
B in dom (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) by A16, ENUMSET1:def 1;
then (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B in rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B by A25, A23, SETFAM_1:def 1;
then A27: m in (EqClass (u,B)) /\ (EqClass (u,C)) by A14, A15, A26, XBOOLE_0:def 4;
m in (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A by A24, A25, A23, SETFAM_1:def 1;
then (EqClass (u,(B '/\' C))) /\ (EqClass (z,A)) <> {} by A8, A9, A27, XBOOLE_0:def 4;
then consider p being object such that
A28: p in (EqClass (u,(B '/\' C))) /\ (EqClass (z,A)) by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A28;
set K = EqClass (p,C);
A29: (EqClass (z,A)) /\ (EqClass (p,C)) in INTERSECTION (A,C) by SETFAM_1:def 5;
set L = EqClass (z,C);
A30: p in EqClass (p,C) by EQREL_1:def 6;
A31: p in EqClass (u,(B '/\' C)) by A28, XBOOLE_0:def 4;
( p in EqClass (p,C) & p in EqClass (z,A) ) by A28, EQREL_1:def 6, XBOOLE_0:def 4;
then A32: p in (EqClass (z,A)) /\ (EqClass (p,C)) by XBOOLE_0:def 4;
then not (EqClass (z,A)) /\ (EqClass (p,C)) in {{}} by TARSKI:def 1;
then (EqClass (z,A)) /\ (EqClass (p,C)) in (INTERSECTION (A,C)) \ {{}} by A29, XBOOLE_0:def 5;
then A33: (EqClass (z,A)) /\ (EqClass (p,C)) in A '/\' C by PARTIT1:def 4;
EqClass (u,(B '/\' C)) c= EqClass (z,C) by A6, BVFUNC11:3;
then EqClass (p,C) meets EqClass (z,C) by A31, A30, XBOOLE_0:3;
then EqClass (p,C) = EqClass (z,C) by EQREL_1:41;
then A34: z in EqClass (p,C) by EQREL_1:def 6;
z in EqClass (z,A) by EQREL_1:def 6;
then A35: z in (EqClass (z,A)) /\ (EqClass (p,C)) by A34, XBOOLE_0:def 4;
CompF (B,G) = A '/\' C by A2, A3, A4, Th5;
then A36: ( (EqClass (z,A)) /\ (EqClass (p,C)) = EqClass (z,(CompF (B,G))) or (EqClass (z,A)) /\ (EqClass (p,C)) misses EqClass (z,(CompF (B,G))) ) by A33, EQREL_1:def 4;
EqClass (u,(B '/\' C)) = EqClass (u,(CompF (A,G))) by A2, A3, A5, Th4;
hence EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G))) by A32, A31, A35, A21, A36, XBOOLE_0:3; :: thesis: verum