let T be Tree; ( ( for n being Element of NAT ex C being finite Chain of T st card C = n ) & ( for t being Element of T holds succ t is finite ) implies ex B being Chain of T st not B is finite )
assume that
A1:
for n being Element of NAT ex X being finite Chain of T st card X = n
and
A2:
for t being Element of T holds succ t is finite
; not for B being Chain of T holds B is finite
defpred S1[ FinSequence] means for n being Element of NAT ex B being Branch of T st
( $1 in B & ex p being FinSequence of NAT st
( p in B & len p >= (len $1) + n ) );
A3:
for x being Element of T st S1[x] holds
ex n being Element of NAT st
( x ^ <*n*> in T & S1[x ^ <*n*>] )
proof
let x be
Element of
T;
( S1[x] implies ex n being Element of NAT st
( x ^ <*n*> in T & S1[x ^ <*n*>] ) )
assume that A4:
S1[
x]
and A5:
for
n being
Element of
NAT st
x ^ <*n*> in T holds
not
S1[
x ^ <*n*>]
;
contradiction
A6:
succ x is
finite
by A2;
defpred S2[
set ,
Element of
NAT ]
means for
B being
Branch of
T for
p,
q being
FinSequence of
NAT st
p = $1 & $1
in B &
q in B holds
(len p) + $2
> len q;
A7:
for
y being
set st
y in succ x holds
ex
n being
Element of
NAT st
S2[
y,
n]
consider f being
Function such that A12:
dom f = succ x
and A13:
for
y being
set st
y in succ x holds
ex
n being
Element of
NAT st
(
f . y = n &
S2[
y,
n] & ( for
m being
Element of
NAT st
S2[
y,
m] holds
n <= m ) )
from TREES_2:sch 4(A7);
consider k being
Element of
NAT such that A14:
for
m being
Element of
NAT st
m in rng f holds
m <= k
by A6, A12, Lm1, FINSET_1:26;
consider B being
Branch of
T such that A15:
x in B
and A16:
ex
p being
FinSequence of
NAT st
(
p in B &
len p >= (len x) + (k + 1) )
by A4;
consider p being
FinSequence of
NAT such that A17:
p in B
and A18:
len p >= (len x) + (k + 1)
by A16;
reconsider r =
p | (Seg ((len x) + 1)) as
FinSequence of
NAT by FINSEQ_1:23;
A19:
(len x) + 1
<= ((len x) + 1) + k
by NAT_1:11;
A20:
len p >= (len x) + 1
by A18, A19, XXREAL_0:2;
A21:
r is_a_prefix_of p
by TREES_1:def 1;
A22:
len r = (len x) + 1
by A20, FINSEQ_1:21;
A23:
r in B
by A17, A21, Th27;
A24:
x is_a_prefix_of r
by A15, A22, A23, Th29, NAT_1:11;
consider j being
FinSequence such that A25:
r = x ^ j
by A24, TREES_1:8;
A26:
(len x) + (len j) = len r
by A25, FINSEQ_1:35;
A27:
j = <*(j . 1)*>
by A22, A26, FINSEQ_1:57;
A28:
(
dom r = Seg (len r) & 1
<= 1
+ (len x) )
by FINSEQ_1:def 3, NAT_1:11;
A29:
(len x) + 1
<= len r
by A20, FINSEQ_1:21;
A30:
(
(x ^ <*(j . 1)*>) . ((len x) + 1) = j . 1 &
(len x) + 1
in dom r )
by A28, A29, FINSEQ_1:3, FINSEQ_1:59;
A31:
j . 1
in rng r
by A25, A27, A30, FUNCT_1:def 5;
reconsider l =
j . 1 as
Element of
NAT by A31;
A32:
x ^ <*l*> in succ x
by A23, A25, A27;
consider n being
Element of
NAT such that A33:
f . (x ^ <*l*>) = n
and A34:
for
B being
Branch of
T for
p,
q being
FinSequence of
NAT st
p = x ^ <*l*> &
x ^ <*l*> in B &
q in B holds
(len p) + n > len q
and
for
m being
Element of
NAT st ( for
B being
Branch of
T for
p,
q being
FinSequence of
NAT st
p = x ^ <*l*> &
x ^ <*l*> in B &
q in B holds
(len p) + m > len q ) holds
n <= m
by A13, A32;
A35:
n in rng f
by A12, A32, A33, FUNCT_1:def 5;
A36:
n <= k
by A14, A35;
A37:
(len r) + n <= ((len x) + 1) + k
by A22, A36, XREAL_1:9;
thus
contradiction
by A17, A18, A23, A25, A27, A34, A37, XXREAL_0:2;
verum
end;
reconsider e = {} as Element of T by TREES_1:47;
A38:
S1[e]
defpred S2[ set ] means ex t being Element of T st
( t = $1 & S1[t] );
defpred S3[ set , set ] means ex p being FinSequence of NAT ex n being Element of NAT st
( $1 = p & p ^ <*n*> in T & $2 = p ^ <*n*> );
A45:
( e in T & S2[e] )
by A38;
A46:
for x being set st x in T & S2[x] holds
ex y being set st
( y in T & S3[x,y] & S2[y] )
proof
let x be
set ;
( x in T & S2[x] implies ex y being set st
( y in T & S3[x,y] & S2[y] ) )
assume
x in T
;
( not S2[x] or ex y being set st
( y in T & S3[x,y] & S2[y] ) )
given t being
Element of
T such that A47:
t = x
and A48:
S1[
t]
;
ex y being set st
( y in T & S3[x,y] & S2[y] )
consider n being
Element of
NAT such that A49:
t ^ <*n*> in T
and A50:
S1[
t ^ <*n*>]
by A3, A48;
reconsider y =
t ^ <*n*> as
set ;
take
y
;
( y in T & S3[x,y] & S2[y] )
thus
(
y in T &
S3[
x,
y] )
by A47, A49;
S2[y]
reconsider t1 =
t ^ <*n*> as
Element of
T by A49;
take
t1
;
( t1 = y & S1[t1] )
thus
(
t1 = y &
S1[
t1] )
by A50;
verum
end;
A51:
ex f being Function st
( dom f = NAT & rng f c= T & f . 0 = e & ( for k being Element of NAT holds
( S3[f . k,f . (k + 1)] & S2[f . k] ) ) )
from TREES_2:sch 5(A45, A46);
consider f being Function such that
A52:
dom f = NAT
and
A53:
rng f c= T
and
A54:
f . 0 = e
and
A55:
for k being Element of NAT holds
( ex p being FinSequence of NAT ex n being Element of NAT st
( f . k = p & p ^ <*n*> in T & f . (k + 1) = p ^ <*n*> ) & ex t being Element of T st
( t = f . k & S1[t] ) )
by A51;
reconsider C = rng f as Subset of T by A53;
A56:
now let k be
Nat;
for n being Nat holds S4[n]defpred S4[
Nat]
means for
p,
q being
FinSequence of
NAT st
p = f . k &
q = f . (k + $1) holds
p is_a_prefix_of q;
A57:
S4[
0 ]
;
A58:
for
n being
Nat st
S4[
n] holds
S4[
n + 1]
proof
let n be
Nat;
( S4[n] implies S4[n + 1] )
assume A59:
for
p,
q being
FinSequence of
NAT st
p = f . k &
q = f . (k + n) holds
p is_a_prefix_of q
;
S4[n + 1]
let p,
q be
FinSequence of
NAT ;
( p = f . k & q = f . (k + (n + 1)) implies p is_a_prefix_of q )
assume that A60:
p = f . k
and A61:
q = f . (k + (n + 1))
;
p is_a_prefix_of q
reconsider k =
k,
n =
n as
Element of
NAT by ORDINAL1:def 13;
consider r being
FinSequence of
NAT ,
l being
Element of
NAT such that A62:
f . (k + n) = r
and
r ^ <*l*> in T
and A63:
f . ((k + n) + 1) = r ^ <*l*>
by A55;
A64:
p is_a_prefix_of r
by A59, A60, A62;
A65:
r is_a_prefix_of r ^ <*l*>
by TREES_1:8;
thus
p is_a_prefix_of q
by A61, A63, A64, A65, XBOOLE_1:1;
verum
end; thus
for
n being
Nat holds
S4[
n]
from NAT_1:sch 2(A57, A58); verum end;
A69:
C is Chain of T
proof
let p be
FinSequence of
NAT ;
TREES_2:def 3 for q being FinSequence of NAT st p in C & q in C holds
p,q are_c=-comparable let q be
FinSequence of
NAT ;
( p in C & q in C implies p,q are_c=-comparable )
assume that A70:
p in C
and A71:
q in C
;
p,q are_c=-comparable
consider x being
set such that A72:
x in NAT
and A73:
p = f . x
by A52, A70, FUNCT_1:def 5;
consider y being
set such that A74:
y in NAT
and A75:
q = f . y
by A52, A71, FUNCT_1:def 5;
reconsider x =
x,
y =
y as
Element of
NAT by A72, A74;
A76:
(
x <= y or
y <= x )
;
thus
(
p is_a_prefix_of q or
q is_a_prefix_of p )
by A66, A73, A75, A76;
XBOOLE_0:def 9 verum
end;
reconsider C = C as Chain of T by A69;
take
C
; not C is finite
defpred S4[ Element of NAT ] means for p being FinSequence of NAT st p = f . $1 holds
len p = $1;
A77:
S4[ 0 ]
by A54;
A78:
for k being Element of NAT st S4[k] holds
S4[k + 1]
A83:
for k being Element of NAT holds S4[k]
from NAT_1:sch 1(A77, A78);
A84:
f is one-to-one
A89:
NAT ,C are_equipotent
by A52, A84, WELLORD2:def 4;
thus
not C is finite
by A89, CARD_1:68; verum