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