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