set D = F2() ^omega ;
reconsider s0 = F3() as Element of F2() by A1;
reconsider f0 = <%s0%> as Element of F2() ^omega by AFINSQ_1:42;
defpred S9[ set , Element of F2() ^omega , Element of F2() ^omega ] means ( ( ( $2 = {} or F1((last $2)) = {} ) implies $2 = $3 ) & ( $2 <> {} & F1((last $2)) <> {} implies ex y being Element of F2() st
( P1[ last $2,y] & F1(y) c< F1((last $2)) & $2 ^ <%y%> = $3 ) ) );
A4:
for a being Nat
for x being Element of F2() ^omega ex y being Element of F2() ^omega st S9[a,x,y]
consider F being sequence of (F2() ^omega) such that
A8:
( F . 0 = f0 & ( for a being Nat holds S9[a,F . a,F . (a + 1)] ) )
from RECDEF_1:sch 2(A4);
defpred S10[ Nat] means F . $1 <> {} ;
A9:
S10[ 0 ]
by A8;
A10:
for m being Nat st S10[m] holds
S10[m + 1]
proof
let m be
Nat;
( S10[m] implies S10[m + 1] )
assume
S10[
m]
;
S10[m + 1]
then reconsider f =
F . m as non
empty Sequence ;
S9[
m,
F . m,
F . (m + 1)]
by A8;
then
(
F . (m + 1) = f or ex
x being
set st
F . (m + 1) = f ^ <%x%> )
;
hence
S10[
m + 1]
;
verum
end;
A11:
for m being Nat holds S10[m]
from NAT_1:sch 2(A9, A10);
defpred S11[ Function] means ( $1 . 0 = F3() & ( for a being Ordinal st succ a in dom $1 holds
ex x, y being Element of F2() st
( x = $1 . a & y = $1 . (succ a) & P1[x,y] ) ) );
defpred S12[ Nat] means S11[F . $1];
A12:
S12[ 0 ]
proof
thus
(F . 0) . 0 = F3()
by A8;
for a being Ordinal st succ a in dom (F . 0) holds
ex x, y being Element of F2() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] )
let a be
Ordinal;
( succ a in dom (F . 0) implies ex x, y being Element of F2() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] ) )
assume
succ a in dom (F . 0)
;
ex x, y being Element of F2() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] )
then
succ a in 1
by A8, AFINSQ_1:def 4;
hence
ex
x,
y being
Element of
F2() st
(
x = (F . 0) . a &
y = (F . 0) . (succ a) &
P1[
x,
y] )
by CARD_1:49, TARSKI:def 1;
verum
end;
A13:
for m being Nat st S12[m] holds
S12[m + 1]
proof
let m be
Nat;
( S12[m] implies S12[m + 1] )
assume A14:
S12[
m]
;
S12[m + 1]
A15:
S9[
m,
F . m,
F . (m + 1)]
by A8;
per cases
( F . m = {} or F1((last (F . m))) = {} or ( F . m <> {} & F1((last (F . m))) <> {} ) )
;
suppose A16:
(
F . m <> {} &
F1(
(last (F . m)))
<> {} )
;
S12[m + 1]reconsider fm =
F . m as non
empty finite Sequence of
F2()
by A16;
reconsider fm1 =
F . (m + 1) as
finite Sequence of
F2() ;
consider y being
Element of
F2()
such that A17:
(
P1[
last fm,
y] &
F1(
y)
c< F1(
(last fm)) &
fm ^ <%y%> = F . (m + 1) )
by A8, A16;
0 in dom fm
by ORDINAL3:8;
hence
(F . (m + 1)) . 0 = F3()
by A14, A17, ORDINAL4:def 1;
for a being Ordinal st succ a in dom (F . (m + 1)) holds
ex x, y being Element of F2() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] )let a be
Ordinal;
( succ a in dom (F . (m + 1)) implies ex x, y being Element of F2() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] ) )assume A18:
succ a in dom (F . (m + 1))
;
ex x, y being Element of F2() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] )A19:
a in succ a
by ORDINAL1:6;
then A20:
a in dom fm1
by A18, ORDINAL1:10;
then reconsider n =
a as
Nat ;
reconsider x =
fm1 . a,
z =
fm1 . (succ a) as
Element of
F2()
by A18, A20, FUNCT_1:102;
A21:
dom <%y%> = 1
by AFINSQ_1:def 4;
then dom fm1 =
(dom fm) +^ 1
by A17, ORDINAL4:def 1
.=
succ (dom fm)
by ORDINAL2:31
;
then A22:
a in dom fm
by A18, ORDINAL3:3;
take
x
;
ex y being Element of F2() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] )take
z
;
( x = (F . (m + 1)) . a & z = (F . (m + 1)) . (succ a) & P1[x,z] )thus
(
x = (F . (m + 1)) . a &
z = (F . (m + 1)) . (succ a) )
;
P1[x,z] end; end;
end;
A28:
for m being Nat holds S12[m]
from NAT_1:sch 2(A12, A13);
defpred S13[ Nat] means ex n being Nat st card F1((last (F . n))) = $1;
A29:
ex n being Nat st S13[n]
A30:
for n being Nat st n <> 0 & S13[n] holds
ex m being Nat st
( m < n & S13[m] )
proof
let n be
Nat;
( n <> 0 & S13[n] implies ex m being Nat st
( m < n & S13[m] ) )
assume A31:
n <> 0
;
( not S13[n] or ex m being Nat st
( m < n & S13[m] ) )
given k being
Nat such that A32:
card F1(
(last (F . k)))
= n
;
ex m being Nat st
( m < n & S13[m] )
reconsider fk =
F . k,
fk1 =
F . (k + 1) as
Element of
F2()
^omega ;
(
S9[
k,
fk,
fk1] &
fk <> {} )
by A11, A8;
then consider y being
Element of
F2()
such that A33:
(
P1[
last fk,
y] &
F1(
y)
c< F1(
(last fk)) &
fk ^ <%y%> = fk1 )
by A31, A32;
A34:
(
F1(
(last fk)) is
finite &
F1(
y)
c= F1(
(last fk)) )
by A32, A33;
A35:
last fk1 = y
by A33, Th81;
then reconsider m =
card F1(
(last fk1)) as
Nat by A34;
take
m
;
( m < n & S13[m] )
thus
m < n
by A32, A33, A34, A35, TREES_1:6;
S13[m]
thus
S13[
m]
;
verum
end;
S13[ 0 ]
from NAT_1:sch 7(A29, A30);
then consider n being Nat such that
A36:
card F1((last (F . n))) = 0
;
reconsider f = F . n as non empty XFinSequence of F2() by A11;
take
f
; ex k being Element of F2() st
( k = last f & F1(k) = {} & f . 0 = F3() & ( for a being Ordinal st succ a in dom f holds
ex x, y being Element of F2() st
( x = f . a & y = f . (succ a) & P1[x,y] ) ) )
reconsider k = last f as Element of F2() by Th79;
take
k
; ( k = last f & F1(k) = {} & f . 0 = F3() & ( for a being Ordinal st succ a in dom f holds
ex x, y being Element of F2() st
( x = f . a & y = f . (succ a) & P1[x,y] ) ) )
thus
( k = last f & F1(k) = {} )
by A36; ( f . 0 = F3() & ( for a being Ordinal st succ a in dom f holds
ex x, y being Element of F2() st
( x = f . a & y = f . (succ a) & P1[x,y] ) ) )
thus
S11[f]
by A28; verum