let Y be non empty set ; for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
let G be Subset of (PARTITIONS Y); for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
let A, B, C, D, E, F, J be a_partition of Y; ( G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J implies CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J )
assume that
A1:
G = {A,B,C,D,E,F,J}
and
A2:
A <> B
and
A3:
A <> C
and
A4:
( A <> D & A <> E )
and
A5:
( A <> F & A <> J )
and
A6:
( B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J )
; CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
A7:
G \ {A} = ({A} \/ {B,C,D,E,F,J}) \ {A}
by A1, ENUMSET1:16;
( not D in {A} & not E in {A} )
by A4, TARSKI:def 1;
then A8:
{D,E} \ {A} = {D,E}
by ZFMISC_1:63;
A9:
( not F in {A} & not J in {A} )
by A5, TARSKI:def 1;
A10:
not C in {A}
by A3, TARSKI:def 1;
A11:
not B in {A}
by A2, TARSKI:def 1;
{B,C,D,E,F,J} \ {A} =
({B} \/ {C,D,E,F,J}) \ {A}
by ENUMSET1:11
.=
({B} \ {A}) \/ ({C,D,E,F,J} \ {A})
by XBOOLE_1:42
.=
{B} \/ ({C,D,E,F,J} \ {A})
by A11, ZFMISC_1:59
.=
{B} \/ (({C} \/ {D,E,F,J}) \ {A})
by ENUMSET1:7
.=
{B} \/ (({C} \ {A}) \/ ({D,E,F,J} \ {A}))
by XBOOLE_1:42
.=
{B} \/ (({C} \ {A}) \/ (({D,E} \/ {F,J}) \ {A}))
by ENUMSET1:5
.=
{B} \/ (({C} \ {A}) \/ (({D,E} \ {A}) \/ ({F,J} \ {A})))
by XBOOLE_1:42
.=
{B} \/ (({C} \ {A}) \/ ({D,E} \/ {F,J}))
by A9, A8, ZFMISC_1:63
.=
{B} \/ ({C} \/ ({D,E} \/ {F,J}))
by A10, ZFMISC_1:59
.=
{B} \/ ({C} \/ {D,E,F,J})
by ENUMSET1:5
.=
{B} \/ {C,D,E,F,J}
by ENUMSET1:7
.=
{B,C,D,E,F,J}
by ENUMSET1:11
;
then A12: G \ {A} =
({A} \ {A}) \/ {B,C,D,E,F,J}
by A7, XBOOLE_1:42
.=
{} \/ {B,C,D,E,F,J}
by XBOOLE_1:37
;
A13:
'/\' (G \ {A}) c= ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
proof
let x be
object ;
TARSKI:def 3 ( not x in '/\' (G \ {A}) or x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J )
reconsider xx =
x as
set by TARSKI:1;
assume
x in '/\' (G \ {A})
;
x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
then consider h being
Function,
FF being
Subset-Family of
Y such that A14:
dom h = G \ {A}
and A15:
rng h = FF
and A16:
for
d being
set st
d in G \ {A} holds
h . d in d
and A17:
x = Intersect FF
and A18:
x <> {}
by BVFUNC_2:def 1;
A19:
C in G \ {A}
by A12, ENUMSET1:def 4;
then A20:
h . C in C
by A16;
set mbcd =
((h . B) /\ (h . C)) /\ (h . D);
A21:
E in G \ {A}
by A12, ENUMSET1:def 4;
then A22:
h . E in rng h
by A14, FUNCT_1:def 3;
set mbc =
(h . B) /\ (h . C);
A23:
B in G \ {A}
by A12, ENUMSET1:def 4;
then
h . B in B
by A16;
then A24:
(h . B) /\ (h . C) in INTERSECTION (
B,
C)
by A20, SETFAM_1:def 5;
A25:
h . B in rng h
by A14, A23, FUNCT_1:def 3;
then A26:
Intersect FF = meet (rng h)
by A15, SETFAM_1:def 9;
A27:
h . C in rng h
by A14, A19, FUNCT_1:def 3;
A28:
F in G \ {A}
by A12, ENUMSET1:def 4;
then A29:
h . F in rng h
by A14, FUNCT_1:def 3;
set mbcdef =
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F);
set mbcde =
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E);
A30:
not
x in {{}}
by A18, TARSKI:def 1;
A31:
J in G \ {A}
by A12, ENUMSET1:def 4;
then A32:
h . J in rng h
by A14, FUNCT_1:def 3;
A33:
D in G \ {A}
by A12, ENUMSET1:def 4;
then A34:
h . D in rng h
by A14, FUNCT_1:def 3;
A35:
xx c= (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)
proof
let m be
object ;
TARSKI:def 3 ( not m in xx or m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) )
assume A36:
m in xx
;
m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)
then
(
m in h . B &
m in h . C )
by A17, A25, A27, A26, SETFAM_1:def 1;
then A37:
m in (h . B) /\ (h . C)
by XBOOLE_0:def 4;
m in h . D
by A17, A34, A26, A36, SETFAM_1:def 1;
then A38:
m in ((h . B) /\ (h . C)) /\ (h . D)
by A37, XBOOLE_0:def 4;
m in h . E
by A17, A22, A26, A36, SETFAM_1:def 1;
then A39:
m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)
by A38, XBOOLE_0:def 4;
m in h . F
by A17, A29, A26, A36, SETFAM_1:def 1;
then A40:
m in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)
by A39, XBOOLE_0:def 4;
m in h . J
by A17, A32, A26, A36, SETFAM_1:def 1;
hence
m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)
by A40, XBOOLE_0:def 4;
verum
end;
then
((h . B) /\ (h . C)) /\ (h . D) <> {}
by A18;
then A41:
not
((h . B) /\ (h . C)) /\ (h . D) in {{}}
by TARSKI:def 1;
(((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) c= xx
proof
A42:
rng h c= {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
proof
let u be
object ;
TARSKI:def 3 ( not u in rng h or u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)} )
assume
u in rng h
;
u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
then consider x1 being
object such that A43:
x1 in dom h
and A44:
u = h . x1
by FUNCT_1:def 3;
(
x1 = B or
x1 = C or
x1 = D or
x1 = E or
x1 = F or
x1 = J )
by A12, A14, A43, ENUMSET1:def 4;
hence
u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
by A44, ENUMSET1:def 4;
verum
end;
let m be
object ;
TARSKI:def 3 ( not m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) or m in xx )
assume A45:
m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)
;
m in xx
then A46:
m in h . J
by XBOOLE_0:def 4;
A47:
m in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)
by A45, XBOOLE_0:def 4;
then A48:
m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)
by XBOOLE_0:def 4;
then A49:
m in h . E
by XBOOLE_0:def 4;
A50:
m in ((h . B) /\ (h . C)) /\ (h . D)
by A48, XBOOLE_0:def 4;
then A51:
m in h . D
by XBOOLE_0:def 4;
m in (h . B) /\ (h . C)
by A50, XBOOLE_0:def 4;
then A52:
(
m in h . B &
m in h . C )
by XBOOLE_0:def 4;
m in h . F
by A47, XBOOLE_0:def 4;
then
for
y being
set st
y in rng h holds
m in y
by A52, A51, A49, A46, A42, ENUMSET1:def 4;
hence
m in xx
by A17, A25, A26, SETFAM_1:def 1;
verum
end;
then A53:
(((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) = x
by A35, XBOOLE_0:def 10;
(h . B) /\ (h . C) <> {}
by A18, A35;
then
not
(h . B) /\ (h . C) in {{}}
by TARSKI:def 1;
then
(h . B) /\ (h . C) in (INTERSECTION (B,C)) \ {{}}
by A24, XBOOLE_0:def 5;
then A54:
(h . B) /\ (h . C) in B '/\' C
by PARTIT1:def 4;
h . D in D
by A16, A33;
then
((h . B) /\ (h . C)) /\ (h . D) in INTERSECTION (
(B '/\' C),
D)
by A54, SETFAM_1:def 5;
then
((h . B) /\ (h . C)) /\ (h . D) in (INTERSECTION ((B '/\' C),D)) \ {{}}
by A41, XBOOLE_0:def 5;
then A55:
((h . B) /\ (h . C)) /\ (h . D) in (B '/\' C) '/\' D
by PARTIT1:def 4;
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) <> {}
by A18, A35;
then A56:
not
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in {{}}
by TARSKI:def 1;
h . E in E
by A16, A21;
then
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in INTERSECTION (
((B '/\' C) '/\' D),
E)
by A55, SETFAM_1:def 5;
then
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in (INTERSECTION (((B '/\' C) '/\' D),E)) \ {{}}
by A56, XBOOLE_0:def 5;
then A57:
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in ((B '/\' C) '/\' D) '/\' E
by PARTIT1:def 4;
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) <> {}
by A18, A35;
then A58:
not
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in {{}}
by TARSKI:def 1;
h . F in F
by A16, A28;
then
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in INTERSECTION (
(((B '/\' C) '/\' D) '/\' E),
F)
by A57, SETFAM_1:def 5;
then
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F)) \ {{}}
by A58, XBOOLE_0:def 5;
then A59:
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in (((B '/\' C) '/\' D) '/\' E) '/\' F
by PARTIT1:def 4;
h . J in J
by A16, A31;
then
x in INTERSECTION (
((((B '/\' C) '/\' D) '/\' E) '/\' F),
J)
by A53, A59, SETFAM_1:def 5;
then
x in (INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J)) \ {{}}
by A30, XBOOLE_0:def 5;
hence
x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
by PARTIT1:def 4;
verum
end;
A60:
((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J c= '/\' (G \ {A})
proof
let x be
object ;
TARSKI:def 3 ( not x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J or x in '/\' (G \ {A}) )
reconsider xx =
x as
set by TARSKI:1;
assume A61:
x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
;
x in '/\' (G \ {A})
then A62:
x <> {}
by EQREL_1:def 4;
x in (INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J)) \ {{}}
by A61, PARTIT1:def 4;
then consider bcdef,
j being
set such that A63:
bcdef in (((B '/\' C) '/\' D) '/\' E) '/\' F
and A64:
j in J
and A65:
x = bcdef /\ j
by SETFAM_1:def 5;
bcdef in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F)) \ {{}}
by A63, PARTIT1:def 4;
then consider bcde,
f being
set such that A66:
bcde in ((B '/\' C) '/\' D) '/\' E
and A67:
f in F
and A68:
bcdef = bcde /\ f
by SETFAM_1:def 5;
bcde in (INTERSECTION (((B '/\' C) '/\' D),E)) \ {{}}
by A66, PARTIT1:def 4;
then consider bcd,
e being
set such that A69:
bcd in (B '/\' C) '/\' D
and A70:
e in E
and A71:
bcde = bcd /\ e
by SETFAM_1:def 5;
bcd in (INTERSECTION ((B '/\' C),D)) \ {{}}
by A69, PARTIT1:def 4;
then consider bc,
d being
set such that A72:
bc in B '/\' C
and A73:
d in D
and A74:
bcd = bc /\ d
by SETFAM_1:def 5;
bc in (INTERSECTION (B,C)) \ {{}}
by A72, PARTIT1:def 4;
then consider b,
c being
set such that A75:
(
b in B &
c in C )
and A76:
bc = b /\ c
by SETFAM_1:def 5;
set h =
(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j);
A77:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B = b
by A6, Th37;
A78:
dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) =
{J,B,C,D,E,F}
by Th38
.=
{J} \/ {B,C,D,E,F}
by ENUMSET1:11
.=
{B,C,D,E,F,J}
by ENUMSET1:15
;
then
D in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by ENUMSET1:def 4;
then A79:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 3;
A80:
for
p being
set st
p in G \ {A} holds
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . p in p
E in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A78, ENUMSET1:def 4;
then A81:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 3;
C in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A78, ENUMSET1:def 4;
then A82:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 3;
A83:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C = c
by A6, Th37;
A84:
rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) c= {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
proof
let t be
object ;
TARSKI:def 3 ( not t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) or t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)} )
assume
t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
;
t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
then consider x1 being
object such that A85:
x1 in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
and A86:
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . x1
by FUNCT_1:def 3;
(
x1 = B or
x1 = C or
x1 = D or
x1 = E or
x1 = F or
x1 = J )
by A78, A85, ENUMSET1:def 4;
hence
t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
by A86, ENUMSET1:def 4;
verum
end;
J in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A78, ENUMSET1:def 4;
then A87:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 3;
F in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A78, ENUMSET1:def 4;
then A88:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 3;
B in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A78, ENUMSET1:def 4;
then A89:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by FUNCT_1:def 3;
{(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)} c= rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
by A79, A89, A82, A81, A88, A87, ENUMSET1:def 4;
then A90:
rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) = {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
by A84, XBOOLE_0:def 10;
A91:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J = j
by A6, Th37;
A92:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F = f
by A6, Th37;
A93:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E = e
by A6, Th37;
A94:
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D = d
by A6, Th37;
rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) c= bool Y
proof
let t be
object ;
TARSKI:def 3 ( not t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) or t in bool Y )
assume
t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j))
;
t in bool Y
then
(
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D or
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B or
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C or
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E or
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F or
t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J )
by A84, ENUMSET1:def 4;
hence
t in bool Y
by A64, A67, A70, A73, A75, A94, A77, A83, A93, A92, A91;
verum
end;
then reconsider FF =
rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) as
Subset-Family of
Y ;
A95:
dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) =
{J,B,C,D,E,F}
by Th38
.=
{J} \/ {B,C,D,E,F}
by ENUMSET1:11
.=
{B,C,D,E,F,J}
by ENUMSET1:15
;
reconsider h =
(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j) as
Function ;
A96:
xx c= Intersect FF
A104:
Intersect FF = meet (rng h)
by A79, SETFAM_1:def 9;
Intersect FF c= xx
proof
let t be
object ;
TARSKI:def 3 ( not t in Intersect FF or t in xx )
assume A105:
t in Intersect FF
;
t in xx
h . C in rng h
by A90, ENUMSET1:def 4;
then A106:
t in c
by A83, A104, A105, SETFAM_1:def 1;
h . B in rng h
by A90, ENUMSET1:def 4;
then
t in b
by A77, A104, A105, SETFAM_1:def 1;
then A107:
t in b /\ c
by A106, XBOOLE_0:def 4;
h . D in rng h
by A90, ENUMSET1:def 4;
then
t in d
by A94, A104, A105, SETFAM_1:def 1;
then A108:
t in (b /\ c) /\ d
by A107, XBOOLE_0:def 4;
h . E in rng h
by A90, ENUMSET1:def 4;
then
t in e
by A93, A104, A105, SETFAM_1:def 1;
then A109:
t in ((b /\ c) /\ d) /\ e
by A108, XBOOLE_0:def 4;
h . F in rng h
by A90, ENUMSET1:def 4;
then
t in f
by A92, A104, A105, SETFAM_1:def 1;
then A110:
t in (((b /\ c) /\ d) /\ e) /\ f
by A109, XBOOLE_0:def 4;
h . J in rng h
by A90, ENUMSET1:def 4;
then
t in j
by A91, A104, A105, SETFAM_1:def 1;
hence
t in xx
by A65, A68, A71, A74, A76, A110, XBOOLE_0:def 4;
verum
end;
then
x = Intersect FF
by A96, XBOOLE_0:def 10;
hence
x in '/\' (G \ {A})
by A12, A95, A80, A62, BVFUNC_2:def 1;
verum
end;
CompF (A,G) = '/\' (G \ {A})
by BVFUNC_2:def 7;
hence
CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
by A60, A13, XBOOLE_0:def 10; verum