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