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
for z, u being Element of Y st G is independent & 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
(EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))) /\ (EqClass (z,A)) <> {}
let G be Subset of (PARTITIONS Y); for A, B, C, D, E, F, J, M, N being a_partition of Y
for z, u being Element of Y st G is independent & 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
(EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))) /\ (EqClass (z,A)) <> {}
let A, B, C, D, E, F, J, M, N be a_partition of Y; for z, u being Element of Y st G is independent & 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
(EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))) /\ (EqClass (z,A)) <> {}
let z, u be Element of Y; ( G is independent & 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 (EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))) /\ (EqClass (z,A)) <> {} )
assume that
A1:
G is independent
and
A2:
G = {A,B,C,D,E,F,J,M,N}
and
A3:
( 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 )
; (EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))) /\ (EqClass (z,A)) <> {}
set h = ((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)));
A4:
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A)
by A3, Th76;
set GG = EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N));
EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = (EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) /\ (EqClass (u,N))
by Th1;
then
EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = ((EqClass (u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J))) /\ (EqClass (u,M))) /\ (EqClass (u,N))
by Th1;
then
EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = (((EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F))) /\ (EqClass (u,J))) /\ (EqClass (u,M))) /\ (EqClass (u,N))
by Th1;
then
EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = ((((EqClass (u,(((B '/\' C) '/\' D) '/\' E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M))) /\ (EqClass (u,N))
by Th1;
then
EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = (((((EqClass (u,((B '/\' C) '/\' D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M))) /\ (EqClass (u,N))
by Th1;
then
EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) = ((((((EqClass (u,(B '/\' C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M))) /\ (EqClass (u,N))
by Th1;
then A5:
(EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))) /\ (EqClass (z,A)) = ((((((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M))) /\ (EqClass (u,N))) /\ (EqClass (z,A))
by Th1;
A6:
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B)
by A3, Th76;
A7:
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . F = EqClass (u,F)
by A3, Th76;
A8:
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . E = EqClass (u,E)
by A3, Th76;
A9:
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . M = EqClass (u,M)
by A3, Th76;
A10:
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . J = EqClass (u,J)
by A3, Th76;
A11:
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . N = EqClass (u,N)
by A3, Th76;
A12:
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D)
by A3, Th76;
A13:
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C)
by A3, Th76;
A14:
rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) = {((((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . A),((((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . B),((((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . C),((((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . D),((((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . E),((((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . F),((((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . J),((((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . M),((((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . N)}
by Th78;
rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) c= bool Y
proof
let t be
object ;
TARSKI:def 3 ( not t in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) or t in bool Y )
assume
t in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
;
t in bool Y
then
(
t = (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . A or
t = (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . B or
t = (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . C or
t = (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . D or
t = (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . E or
t = (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . F or
t = (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . J or
t = (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . M or
t = (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . N )
by A14, ENUMSET1:def 7;
hence
t in bool Y
by A4, A6, A13, A12, A8, A7, A10, A9, A11;
verum
end;
then reconsider FF = rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) as Subset-Family of Y ;
A15:
dom (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) = G
by A2, Th77;
then
A in dom (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by A2, ENUMSET1:def 7;
then A16:
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . A in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by FUNCT_1:def 3;
then A17:
Intersect FF = meet (rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))))
by SETFAM_1:def 9;
for d being set st d in G holds
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . d in d
proof
let d be
set ;
( d in G implies (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . d in d )
assume
d in G
;
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . d in d
then
(
d = A or
d = B or
d = C or
d = D or
d = E or
d = F or
d = J or
d = M or
d = N )
by A2, ENUMSET1:def 7;
hence
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . d in d
by A4, A6, A13, A12, A8, A7, A10, A9, A11;
verum
end;
then
Intersect FF <> {}
by A1, A15, BVFUNC_2:def 5;
then consider m being object such that
A18:
m in Intersect FF
by XBOOLE_0:def 1;
C in dom (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by A2, A15, ENUMSET1:def 7;
then
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . C in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by FUNCT_1:def 3;
then A19:
m in EqClass (u,C)
by A13, A17, A18, SETFAM_1:def 1;
B in dom (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by A2, A15, ENUMSET1:def 7;
then
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . B in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by FUNCT_1:def 3;
then
m in EqClass (u,B)
by A6, A17, A18, SETFAM_1:def 1;
then A20:
m in (EqClass (u,B)) /\ (EqClass (u,C))
by A19, XBOOLE_0:def 4;
D in dom (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by A2, A15, ENUMSET1:def 7;
then
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . D in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by FUNCT_1:def 3;
then
m in EqClass (u,D)
by A12, A17, A18, SETFAM_1:def 1;
then A21:
m in ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))
by A20, XBOOLE_0:def 4;
E in dom (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by A2, A15, ENUMSET1:def 7;
then
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . E in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by FUNCT_1:def 3;
then
m in EqClass (u,E)
by A8, A17, A18, SETFAM_1:def 1;
then A22:
m in (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))
by A21, XBOOLE_0:def 4;
F in dom (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by A2, A15, ENUMSET1:def 7;
then
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . F in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by FUNCT_1:def 3;
then
m in EqClass (u,F)
by A7, A17, A18, SETFAM_1:def 1;
then A23:
m in ((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))
by A22, XBOOLE_0:def 4;
J in dom (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by A2, A15, ENUMSET1:def 7;
then
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . J in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by FUNCT_1:def 3;
then
m in EqClass (u,J)
by A10, A17, A18, SETFAM_1:def 1;
then A24:
m in (((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))
by A23, XBOOLE_0:def 4;
M in dom (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by A2, A15, ENUMSET1:def 7;
then
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . M in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by FUNCT_1:def 3;
then
m in EqClass (u,M)
by A9, A17, A18, SETFAM_1:def 1;
then A25:
m in ((((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M))
by A24, XBOOLE_0:def 4;
N in dom (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by A2, A15, ENUMSET1:def 7;
then
(((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A)))) . N in rng (((((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (F .--> (EqClass (u,F)))) +* (J .--> (EqClass (u,J)))) +* (M .--> (EqClass (u,M)))) +* (N .--> (EqClass (u,N)))) +* (A .--> (EqClass (z,A))))
by FUNCT_1:def 3;
then
m in EqClass (u,N)
by A11, A17, A18, SETFAM_1:def 1;
then A26:
m in (((((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (u,F))) /\ (EqClass (u,J))) /\ (EqClass (u,M))) /\ (EqClass (u,N))
by A25, XBOOLE_0:def 4;
m in EqClass (z,A)
by A4, A16, A17, A18, SETFAM_1:def 1;
hence
(EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))) /\ (EqClass (z,A)) <> {}
by A5, A26, XBOOLE_0:def 4; verum