let Y be non empty set ; for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E holds
CompF (A,G) = ((B '/\' C) '/\' D) '/\' E
let G be Subset of (PARTITIONS Y); for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E holds
CompF (A,G) = ((B '/\' C) '/\' D) '/\' E
let A, B, C, D, E be a_partition of Y; ( G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E implies CompF (A,G) = ((B '/\' C) '/\' D) '/\' E )
assume that
A1:
G = {A,B,C,D,E}
and
A2:
A <> B
and
A3:
A <> C
and
A4:
A <> D
and
A5:
A <> E
; CompF (A,G) = ((B '/\' C) '/\' D) '/\' E
per cases
( B = C or B = D or B = E or C = D or C = E or D = E or ( B <> C & B <> D & B <> E & C <> D & C <> E & D <> E ) )
;
suppose A6:
B = C
;
CompF (A,G) = ((B '/\' C) '/\' D) '/\' Ethen G =
{A,B,B,D} \/ {E}
by A1, ENUMSET1:10
.=
{B,B,A,D} \/ {E}
by ENUMSET1:67
.=
{B,B,A,D,E}
by ENUMSET1:10
.=
{B,A,D,E}
by ENUMSET1:32
.=
{A,B,D,E}
by ENUMSET1:65
;
hence CompF (
A,
G) =
(B '/\' D) '/\' E
by A2, A4, A5, Th7
.=
((B '/\' C) '/\' D) '/\' E
by A6, PARTIT1:13
;
verum end; suppose A7:
B = D
;
CompF (A,G) = ((B '/\' C) '/\' D) '/\' Ethen G =
{A,B,C,B} \/ {E}
by A1, ENUMSET1:10
.=
{B,B,A,C} \/ {E}
by ENUMSET1:69
.=
{B,B,A,C,E}
by ENUMSET1:10
.=
{B,A,C,E}
by ENUMSET1:32
.=
{A,B,C,E}
by ENUMSET1:65
;
hence CompF (
A,
G) =
(B '/\' C) '/\' E
by A2, A3, A5, Th7
.=
((B '/\' D) '/\' C) '/\' E
by A7, PARTIT1:13
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:14
;
verum end; suppose A8:
B = E
;
CompF (A,G) = ((B '/\' C) '/\' D) '/\' Ethen G =
{A} \/ {B,C,D,B}
by A1, ENUMSET1:7
.=
{A} \/ {B,B,C,D}
by ENUMSET1:63
.=
{A} \/ {B,C,D}
by ENUMSET1:31
.=
{A,B,C,D}
by ENUMSET1:4
;
hence CompF (
A,
G) =
(B '/\' C) '/\' D
by A2, A3, A4, Th7
.=
((B '/\' E) '/\' C) '/\' D
by A8, PARTIT1:13
.=
(B '/\' E) '/\' (C '/\' D)
by PARTIT1:14
.=
(B '/\' (C '/\' D)) '/\' E
by PARTIT1:14
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:14
;
verum end; suppose A9:
C = D
;
CompF (A,G) = ((B '/\' C) '/\' D) '/\' Ethen G =
{A,B,C,C} \/ {E}
by A1, ENUMSET1:10
.=
{C,C,A,B} \/ {E}
by ENUMSET1:73
.=
{C,A,B} \/ {E}
by ENUMSET1:31
.=
{C,A,B,E}
by ENUMSET1:6
.=
{A,B,C,E}
by ENUMSET1:67
;
hence CompF (
A,
G) =
(B '/\' C) '/\' E
by A2, A3, A5, Th7
.=
(B '/\' (C '/\' D)) '/\' E
by A9, PARTIT1:13
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:14
;
verum end; suppose A10:
C = E
;
CompF (A,G) = ((B '/\' C) '/\' D) '/\' Ethen G =
{A} \/ {B,C,D,C}
by A1, ENUMSET1:7
.=
{A} \/ {C,C,B,D}
by ENUMSET1:72
.=
{A} \/ {C,B,D}
by ENUMSET1:31
.=
{A,C,B,D}
by ENUMSET1:4
.=
{A,B,C,D}
by ENUMSET1:62
;
hence CompF (
A,
G) =
(B '/\' C) '/\' D
by A2, A3, A4, Th7
.=
(B '/\' (C '/\' E)) '/\' D
by A10, PARTIT1:13
.=
B '/\' ((C '/\' E) '/\' D)
by PARTIT1:14
.=
B '/\' ((C '/\' D) '/\' E)
by PARTIT1:14
.=
(B '/\' (C '/\' D)) '/\' E
by PARTIT1:14
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:14
;
verum end; suppose A11:
D = E
;
CompF (A,G) = ((B '/\' C) '/\' D) '/\' Ethen G =
{A} \/ {B,C,D,D}
by A1, ENUMSET1:7
.=
{A} \/ {D,D,B,C}
by ENUMSET1:73
.=
{A} \/ {D,B,C}
by ENUMSET1:31
.=
{A,D,B,C}
by ENUMSET1:4
.=
{A,B,C,D}
by ENUMSET1:63
;
hence CompF (
A,
G) =
(B '/\' C) '/\' D
by A2, A3, A4, Th7
.=
(B '/\' C) '/\' (D '/\' E)
by A11, PARTIT1:13
.=
B '/\' (C '/\' (D '/\' E))
by PARTIT1:14
.=
B '/\' ((C '/\' D) '/\' E)
by PARTIT1:14
.=
(B '/\' (C '/\' D)) '/\' E
by PARTIT1:14
.=
((B '/\' C) '/\' D) '/\' E
by PARTIT1:14
;
verum end; suppose A12:
(
B <> C &
B <> D &
B <> E &
C <> D &
C <> E &
D <> E )
;
CompF (A,G) = ((B '/\' C) '/\' D) '/\' EA13:
( not
D in {A} & not
E in {A} )
by A4, A5, TARSKI:def 1;
A14:
not
B in {A}
by A2, TARSKI:def 1;
G \ {A} = ({A} \/ {B,C,D,E}) \ {A}
by A1, ENUMSET1:7;
then A15:
G \ {A} = ({A} \ {A}) \/ ({B,C,D,E} \ {A})
by XBOOLE_1:42;
A16:
not
C in {A}
by A3, TARSKI:def 1;
A in {A}
by TARSKI:def 1;
then A17:
{A} \ {A} = {}
by ZFMISC_1:60;
{B,C,D,E} \ {A} =
({B} \/ {C,D,E}) \ {A}
by ENUMSET1:4
.=
({B} \ {A}) \/ ({C,D,E} \ {A})
by XBOOLE_1:42
.=
{B} \/ ({C,D,E} \ {A})
by A14, ZFMISC_1:59
.=
{B} \/ (({C} \/ {D,E}) \ {A})
by ENUMSET1:2
.=
{B} \/ (({C} \ {A}) \/ ({D,E} \ {A}))
by XBOOLE_1:42
.=
{B} \/ (({C} \ {A}) \/ {D,E})
by A13, ZFMISC_1:63
.=
{B} \/ ({C} \/ {D,E})
by A16, ZFMISC_1:59
.=
{B} \/ {C,D,E}
by ENUMSET1:2
;
then A18:
G \ {A} = ({A} \ {A}) \/ {B,C,D,E}
by A15, ENUMSET1:4;
A19:
((B '/\' C) '/\' D) '/\' E c= '/\' (G \ {A})
proof
let x be
object ;
TARSKI:def 3 ( not x in ((B '/\' C) '/\' D) '/\' E or x in '/\' (G \ {A}) )
reconsider xx =
x as
set by TARSKI:1;
assume A20:
x in ((B '/\' C) '/\' D) '/\' E
;
x in '/\' (G \ {A})
then A21:
x <> {}
by EQREL_1:def 4;
x in (INTERSECTION (((B '/\' C) '/\' D),E)) \ {{}}
by A20, PARTIT1:def 4;
then consider bcd,
e being
set such that A22:
bcd in (B '/\' C) '/\' D
and A23:
e in E
and A24:
x = bcd /\ e
by SETFAM_1:def 5;
bcd in (INTERSECTION ((B '/\' C),D)) \ {{}}
by A22, PARTIT1:def 4;
then consider bc,
d being
set such that A25:
bc in B '/\' C
and A26:
d in D
and A27:
bcd = bc /\ d
by SETFAM_1:def 5;
bc in (INTERSECTION (B,C)) \ {{}}
by A25, PARTIT1:def 4;
then consider b,
c being
set such that A28:
b in B
and A29:
c in C
and A30:
bc = b /\ c
by SETFAM_1:def 5;
set h =
(((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e);
A32:
C in dom (C .--> c)
by TARSKI:def 1;
A34:
D in dom (D .--> d)
by TARSKI:def 1;
A35:
not
C in dom (D .--> d)
by A12, TARSKI:def 1;
E in dom (E .--> e)
by TARSKI:def 1;
then A37:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E = (E .--> e) . E
by FUNCT_4:13;
then A38:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E = e
by FUNCOP_1:72;
not
C in dom (E .--> e)
by A12, TARSKI:def 1;
then
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C
by FUNCT_4:11;
then
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = ((B .--> b) +* (C .--> c)) . C
by A35, FUNCT_4:11;
then A39:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = (C .--> c) . C
by A32, FUNCT_4:13;
then A40:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = c
by FUNCOP_1:72;
not
D in dom (E .--> e)
by A12, TARSKI:def 1;
then
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D
by FUNCT_4:11;
then A41:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D = (D .--> d) . D
by A34, FUNCT_4:13;
then A42:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D = d
by FUNCOP_1:72;
A43:
not
B in dom (C .--> c)
by A12, TARSKI:def 1;
A44:
not
B in dom (D .--> d)
by A12, TARSKI:def 1;
not
B in dom (E .--> e)
by A12, TARSKI:def 1;
then
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B
by FUNCT_4:11;
then
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = ((B .--> b) +* (C .--> c)) . B
by A44, FUNCT_4:11;
then A45:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = (B .--> b) . B
by A43, FUNCT_4:11;
then A46:
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = b
by FUNCOP_1:72;
A47:
for
p being
set st
p in G \ {A} holds
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . p in p
dom ((B .--> b) +* (C .--> c)) = (dom (B .--> b)) \/ (dom (C .--> c))
by FUNCT_4:def 1;
then
dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = ((dom (B .--> b)) \/ (dom (C .--> c))) \/ (dom (D .--> d))
by FUNCT_4:def 1;
then A49:
dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) = (((dom (B .--> b)) \/ (dom (C .--> c))) \/ (dom (D .--> d))) \/ (dom (E .--> e))
by FUNCT_4:def 1;
A50:
dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) =
(({B} \/ {C}) \/ {D}) \/ {E}
by A49
.=
({B,C} \/ {D}) \/ {E}
by ENUMSET1:1
.=
{B,C,D} \/ {E}
by ENUMSET1:3
.=
{B,C,D,E}
by ENUMSET1:6
;
then A51:
D in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by ENUMSET1:def 2;
A52:
rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) c= {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)}
proof
let t be
object ;
TARSKI:def 3 ( not t in rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) or t in {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} )
assume
t in rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
;
t in {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)}
then consider x1 being
object such that A53:
x1 in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
and A54:
t = ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . x1
by FUNCT_1:def 3;
now ( ( x1 = D & t in {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} ) or ( x1 = B & t in {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} ) or ( x1 = C & t in {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} ) or ( x1 = E & t in {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} ) )end;
hence
t in {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)}
;
verum
end;
rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) c= bool Y
then reconsider F =
rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) as
Subset-Family of
Y ;
A56:
C in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A50, ENUMSET1:def 2;
A57:
E in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A50, ENUMSET1:def 2;
A58:
B in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A50, ENUMSET1:def 2;
A59:
{(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} c= rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
then A61:
{(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} = rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e))
by A52, XBOOLE_0:def 10;
reconsider h =
(((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e) as
Function ;
A62:
xx c= Intersect F
A69:
rng h <> {}
by A51, FUNCT_1:3;
Intersect F c= xx
proof
let t be
object ;
TARSKI:def 3 ( not t in Intersect F or t in xx )
assume
t in Intersect F
;
t in xx
then A70:
t in meet (rng h)
by A69, SETFAM_1:def 9;
h . D in rng h
by A61, ENUMSET1:def 2;
then A71:
t in h . D
by A70, SETFAM_1:def 1;
h . C in rng h
by A61, ENUMSET1:def 2;
then A72:
t in h . C
by A70, SETFAM_1:def 1;
h . B in rng h
by A61, ENUMSET1:def 2;
then
t in h . B
by A70, SETFAM_1:def 1;
then
t in b /\ c
by A46, A40, A72, XBOOLE_0:def 4;
then A73:
t in (b /\ c) /\ d
by A42, A71, XBOOLE_0:def 4;
h . E in rng h
by A61, ENUMSET1:def 2;
then
t in h . E
by A70, SETFAM_1:def 1;
hence
t in xx
by A24, A27, A30, A38, A73, XBOOLE_0:def 4;
verum
end;
then
x = Intersect F
by A62, XBOOLE_0:def 10;
hence
x in '/\' (G \ {A})
by A18, A17, A50, A47, A21, BVFUNC_2:def 1;
verum
end;
'/\' (G \ {A}) c= ((B '/\' C) '/\' D) '/\' E
proof
let x be
object ;
TARSKI:def 3 ( not x in '/\' (G \ {A}) or x in ((B '/\' C) '/\' D) '/\' E )
reconsider xx =
x as
set by TARSKI:1;
assume
x in '/\' (G \ {A})
;
x in ((B '/\' C) '/\' D) '/\' E
then consider h being
Function,
F being
Subset-Family of
Y such that A74:
dom h = G \ {A}
and A75:
rng h = F
and A76:
for
d being
set st
d in G \ {A} holds
h . d in d
and A77:
x = Intersect F
and A78:
x <> {}
by BVFUNC_2:def 1;
D in dom h
by A18, A17, A74, ENUMSET1:def 2;
then A79:
h . D in rng h
by FUNCT_1:def 3;
set mbc =
(h . B) /\ (h . C);
A80:
not
x in {{}}
by A78, TARSKI:def 1;
E in G \ {A}
by A18, A17, ENUMSET1:def 2;
then A81:
h . E in E
by A76;
D in G \ {A}
by A18, A17, ENUMSET1:def 2;
then A82:
h . D in D
by A76;
C in G \ {A}
by A18, A17, ENUMSET1:def 2;
then A83:
h . C in C
by A76;
E in dom h
by A18, A17, A74, ENUMSET1:def 2;
then A84:
h . E in rng h
by FUNCT_1:def 3;
set mbcd =
((h . B) /\ (h . C)) /\ (h . D);
B in dom h
by A18, A17, A74, ENUMSET1:def 2;
then A85:
h . B in rng h
by FUNCT_1:def 3;
C in dom h
by A18, A17, A74, ENUMSET1:def 2;
then A86:
h . C in rng h
by FUNCT_1:def 3;
A87:
xx c= (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)
proof
let m be
object ;
TARSKI:def 3 ( not m in xx or m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) )
assume
m in xx
;
m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)
then A88:
m in meet (rng h)
by A75, A77, A85, SETFAM_1:def 9;
then
(
m in h . B &
m in h . C )
by A85, A86, SETFAM_1:def 1;
then A89:
m in (h . B) /\ (h . C)
by XBOOLE_0:def 4;
m in h . D
by A79, A88, SETFAM_1:def 1;
then A90:
m in ((h . B) /\ (h . C)) /\ (h . D)
by A89, XBOOLE_0:def 4;
m in h . E
by A84, A88, SETFAM_1:def 1;
hence
m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)
by A90, XBOOLE_0:def 4;
verum
end;
then
((h . B) /\ (h . C)) /\ (h . D) <> {}
by A78;
then A91:
not
((h . B) /\ (h . C)) /\ (h . D) in {{}}
by TARSKI:def 1;
(h . B) /\ (h . C) <> {}
by A78, A87;
then A92:
not
(h . B) /\ (h . C) in {{}}
by TARSKI:def 1;
B in G \ {A}
by A18, A17, ENUMSET1:def 2;
then
h . B in B
by A76;
then
(h . B) /\ (h . C) in INTERSECTION (
B,
C)
by A83, SETFAM_1:def 5;
then
(h . B) /\ (h . C) in (INTERSECTION (B,C)) \ {{}}
by A92, XBOOLE_0:def 5;
then
(h . B) /\ (h . C) in B '/\' C
by PARTIT1:def 4;
then
((h . B) /\ (h . C)) /\ (h . D) in INTERSECTION (
(B '/\' C),
D)
by A82, SETFAM_1:def 5;
then
((h . B) /\ (h . C)) /\ (h . D) in (INTERSECTION ((B '/\' C),D)) \ {{}}
by A91, XBOOLE_0:def 5;
then A93:
((h . B) /\ (h . C)) /\ (h . D) in (B '/\' C) '/\' D
by PARTIT1:def 4;
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) c= xx
proof
let m be
object ;
TARSKI:def 3 ( not m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) or m in xx )
assume A94:
m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)
;
m in xx
then A95:
m in ((h . B) /\ (h . C)) /\ (h . D)
by XBOOLE_0:def 4;
then A96:
m in (h . B) /\ (h . C)
by XBOOLE_0:def 4;
A97:
rng h c= {(h . B),(h . C),(h . D),(h . E)}
proof
let u be
object ;
TARSKI:def 3 ( not u in rng h or u in {(h . B),(h . C),(h . D),(h . E)} )
assume
u in rng h
;
u in {(h . B),(h . C),(h . D),(h . E)}
then consider x1 being
object such that A98:
x1 in dom h
and A99:
u = h . x1
by FUNCT_1:def 3;
now ( ( x1 = B & u in {(h . B),(h . C),(h . D),(h . E)} ) or ( x1 = C & u in {(h . B),(h . C),(h . D),(h . E)} ) or ( x1 = D & u in {(h . B),(h . C),(h . D),(h . E)} ) or ( x1 = E & u in {(h . B),(h . C),(h . D),(h . E)} ) )end;
hence
u in {(h . B),(h . C),(h . D),(h . E)}
;
verum
end;
for
y being
set st
y in rng h holds
m in y
proof
let y be
set ;
( y in rng h implies m in y )
assume A100:
y in rng h
;
m in y
now ( ( y = h . B & m in y ) or ( y = h . C & m in y ) or ( y = h . D & m in y ) or ( y = h . E & m in y ) )end;
hence
m in y
;
verum
end;
then
m in meet (rng h)
by A85, SETFAM_1:def 1;
hence
m in xx
by A75, A77, A85, SETFAM_1:def 9;
verum
end;
then
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) = x
by A87, XBOOLE_0:def 10;
then
x in INTERSECTION (
((B '/\' C) '/\' D),
E)
by A81, A93, SETFAM_1:def 5;
then
x in (INTERSECTION (((B '/\' C) '/\' D),E)) \ {{}}
by A80, XBOOLE_0:def 5;
hence
x in ((B '/\' C) '/\' D) '/\' E
by PARTIT1:def 4;
verum
end; then
'/\' (G \ {A}) = ((B '/\' C) '/\' D) '/\' E
by A19, XBOOLE_0:def 10;
hence
CompF (
A,
G)
= ((B '/\' C) '/\' D) '/\' E
by BVFUNC_2:def 7;
verum end;