set N = { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ;
deffunc H1( Element of (Free (S,Y))) -> set = vf S;
A0:
rng D is finite
;
A1:
{ H1(v) where v is Element of (Free (S,Y)) : v in rng D } is finite
from FRAENKEL:sch 21(A0);
A3:
{ (vf v) where v is Element of (Free (S,Y)) : v in rng D } is finite-membered
deffunc H2( Element of dom B, set ) -> set = { the Element of (Y . (B . (S + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ Y)} \/ Y;
consider g being non empty FinSequence such that
A2:
( dom g = dom B & g . 1 = { the Element of (Y . (B . 1)) \ ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V))} & ( for i, j being Element of dom B st j = i + 1 holds
g . j = H2(i,g . i) ) )
from MSAFREE5:sch 7();
deffunc H3( Element of dom B, set ) -> set = union ((g . (S + 1)) \ (g . S));
consider f being non empty FinSequence such that
AA:
( dom f = dom B & f . 1 = union (g . 1) & ( for i, j being Element of dom B st j = i + 1 holds
f . j = H3(i,f . i) ) )
from MSAFREE5:sch 7();
defpred S1[ Nat] means ( S in dom B implies g . S is finite );
B1:
S1[1]
by A2;
B2:
for i being Nat st i >= 1 & S1[i] holds
S1[i + 1]
B3:
for i being Nat st i >= 1 holds
S1[i]
from NAT_1:sch 8(B1, B2);
defpred S2[ Nat] means ( S + 1 in dom B implies ( g . (S + 1) = {(f . (S + 1))} \/ (g . S) & f . (S + 1) nin g . S & f . (S + 1) = the Element of (Y . (B . (S + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . S)) ) );
C1:
S2[1]
proof
assume C2:
1
+ 1
in dom B
;
( g . (1 + 1) = {(f . (1 + 1))} \/ (g . 1) & f . (1 + 1) nin g . 1 & f . (1 + 1) = the Element of (Y . (B . (1 + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . 1)) )
then
1
+ 1
<= len B
by FINSEQ_3:25;
then
1
<= len B
by XXREAL_0:2;
then reconsider i = 1,
j = 1
+ 1 as
Element of
dom B by C2, FINSEQ_3:25;
reconsider gi =
g . i as
finite set by A2;
set x = the
Element of
(Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi);
C6:
the
Element of
(Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi) nin ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi
by A1, A3, XBOOLE_0:def 5;
then C3:
the
Element of
(Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi) nin g . i
by XBOOLE_0:def 3;
(
g . 2
= H2(
i,
g . 1) &
H2(
i,
g . 1)
= { the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi)} \/ (g . 1) &
f . 2
= H3(
i,
f . 1) &
H3(
i,
f . 1)
= union ((g . (i + 1)) \ (g . i)) )
by A2, AA, C2;
then
(
f . 2
= union { the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi)} &
union { the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi)} = the
Element of
(Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi) )
by C3, EXCHSORT:3;
hence
(
g . (1 + 1) = {(f . (1 + 1))} \/ (g . 1) &
f . (1 + 1) nin g . 1 &
f . (1 + 1) = the
Element of
(Y . (B . (1 + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . 1)) )
by C6, A2, XBOOLE_0:def 3;
verum
end;
C5:
for i being Nat st i >= 1 & S2[i] holds
S2[i + 1]
proof
let i be
Nat;
( i >= 1 & S2[i] implies S2[i + 1] )
assume Z0:
i >= 1
;
( not S2[i] or S2[i + 1] )
assume
S2[
i]
;
S2[i + 1]
assume Z2:
(i + 1) + 1
in dom B
;
( g . ((i + 1) + 1) = {(f . ((i + 1) + 1))} \/ (g . (i + 1)) & f . ((i + 1) + 1) nin g . (i + 1) & f . ((i + 1) + 1) = the Element of (Y . (B . ((i + 1) + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . (i + 1))) )
then
(
i + 1
<= (i + 1) + 1 &
(i + 1) + 1
<= len B )
by NAT_1:12, FINSEQ_3:25;
then C6:
( 1
<= i + 1 &
i + 1
<= len B )
by NAT_1:12, XXREAL_0:2;
then reconsider j2 =
(i + 1) + 1,
j = 1
+ i as
Element of
dom B by Z2, FINSEQ_3:25;
i <= i + 1
by NAT_1:12;
then
i <= len B
by C6, XXREAL_0:2;
then
i in dom B
by Z0, FINSEQ_3:25;
then reconsider gi =
g . i,
gj =
g . j as
finite set by B3, FINSEQ_3:25;
set x = the
Element of
(Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj);
C7:
the
Element of
(Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj) nin ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj
by A1, A3, XBOOLE_0:def 5;
then C3:
the
Element of
(Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj) nin g . j
by XBOOLE_0:def 3;
(
g . j2 = H2(
j,
g . j) &
H2(
j,
g . j)
= { the Element of (Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj)} \/ (g . j) &
f . j2 = H3(
j,
f . j) &
H3(
j,
f . j)
= union ((g . (j + 1)) \ (g . j)) )
by A2, AA;
then
(
f . j2 = union { the Element of (Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj)} &
union { the Element of (Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj)} = the
Element of
(Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj) )
by C3, EXCHSORT:3;
hence
(
g . ((i + 1) + 1) = {(f . ((i + 1) + 1))} \/ (g . (i + 1)) &
f . ((i + 1) + 1) nin g . (i + 1) &
f . ((i + 1) + 1) = the
Element of
(Y . (B . ((i + 1) + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . (i + 1))) )
by C7, A2, XBOOLE_0:def 3;
verum
end;
C7:
for i being Nat st i >= 1 holds
S2[i]
from NAT_1:sch 8(C1, C5);
rng f c= Union Y
proof
let a be
object ;
TARSKI:def 3 ( not a in rng f or a in Union Y )
assume
a in rng f
;
a in Union Y
then consider b being
object such that A5:
(
b in dom f &
a = f . b )
by FUNCT_1:def 3;
reconsider b =
b as
Element of
dom B by AA, A5;
b >= 1
by FINSEQ_3:25;
per cases then
( b = 1 or b > 1 )
by XXREAL_0:1;
suppose
b > 1
;
a in Union Ythen
b >= 1
+ 1
by NAT_1:13;
then consider c being
Nat such that D1:
b = (1 + 1) + c
by NAT_1:10;
D2:
b = (1 + c) + 1
by D1;
then
(
len B >= b &
b > 1
+ c )
by NAT_1:13, FINSEQ_3:25;
then
(
len B >= 1
+ c & 1
+ c >= 1 )
by NAT_1:12, XXREAL_0:2;
then reconsider c1 = 1
+ c as
Element of
dom B by FINSEQ_3:25;
g . c1 is
finite
by B3, FINSEQ_3:25;
then
(
a = the
Element of
(Y . (B . b)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)) &
(Y . (B . b)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)) <> {} )
by C6, A1, A3, D2, A5;
then
(
a in Y . (B . b) &
B . b in the
carrier of
S & the
carrier of
S = dom Y )
by XBOOLE_0:def 5, PARTFUN1:def 2;
hence
a in Union Y
by CARD_5:2;
verum end; end;
end;
then reconsider f = f as FinSequence of Union Y by FINSEQ_1:def 4;
E0:
for i, j being Element of dom B st i <= j holds
g . i c= g . j
F0:
for i, j being Element of dom B st i < j holds
( f . j nin g . i & f . j in g . j )
F1:
for b being Element of dom B holds f . b in g . b
f is B -sorts
then reconsider f = f as B -sorts FinSequence of Union Y ;
take
f
; ( f is one-to-one & f is V -omitting & f is D -omitting )
thus
f is one-to-one
( f is V -omitting & f is D -omitting )
now for a being object st a in rng f holds
a nin (union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)let a be
object ;
( a in rng f implies b1 nin (union { (vf b2) where v is Element of (Free (S,Y)) : b2 in rng D } ) \/ (rng V) )assume
a in rng f
;
b1 nin (union { (vf b2) where v is Element of (Free (S,Y)) : b2 in rng D } ) \/ (rng V)then consider b being
object such that A5:
(
b in dom f &
a = f . b )
by FUNCT_1:def 3;
reconsider b =
b as
Element of
dom B by AA, A5;
1
<= b
by FINSEQ_3:25;
per cases then
( b = 1 or b > 1 )
by XXREAL_0:1;
suppose
b > 1
;
b1 nin (union { (vf b2) where v is Element of (Free (S,Y)) : b2 in rng D } ) \/ (rng V)then
b >= 1
+ 1
by NAT_1:13;
then consider c being
Nat such that D1:
b = (1 + 1) + c
by NAT_1:10;
D2:
b = (1 + c) + 1
by D1;
then
(
len B >= b &
b > 1
+ c )
by NAT_1:13, FINSEQ_3:25;
then
(
len B >= 1
+ c & 1
+ c >= 1 )
by NAT_1:12, XXREAL_0:2;
then reconsider c1 = 1
+ c as
Element of
dom B by FINSEQ_3:25;
g . c1 is
finite
by B3, FINSEQ_3:25;
then
(
a = the
Element of
(Y . (B . b)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)) &
(Y . (B . b)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)) <> {} )
by C6, A1, A3, D2, A5;
then
a nin ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)
by XBOOLE_0:def 5;
hence
a nin (union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)
by XBOOLE_0:def 3;
verum end; end; end;
then A4:
rng f misses (union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)
by XBOOLE_0:3;
thus
rng V misses rng f
by A4, XBOOLE_1:7, XBOOLE_1:63; MSAFREE5:def 39 f is D -omitting
let t be Element of (Free (S,Y)); MSAFREE5:def 41 ( t in rng D implies vf t misses rng f )
assume
t in rng D
; vf t misses rng f
then
vf t in { (vf v) where v is Element of (Free (S,Y)) : v in rng D }
;
then
vf t c= union { (vf v) where v is Element of (Free (S,Y)) : v in rng D }
by ZFMISC_1:74;
hence
vf t misses rng f
by A4, XBOOLE_1:10, XBOOLE_1:63; verum