let T be Tree; ( ( for n being 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 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 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 Nat st
( x ^ <*n*> in T & S1[x ^ <*n*>] )
proof
let x be
Element of
T;
( S1[x] implies ex n being Nat st
( x ^ <*n*> in T & S1[x ^ <*n*>] ) )
assume that A4:
S1[
x]
and A5:
for
n being
Nat st
x ^ <*n*> in T holds
not
S1[
x ^ <*n*>]
;
contradiction
A6:
succ x is
finite
by A2;
defpred S2[
object ,
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
object st
y in succ x holds
ex
n being
Nat st
S2[
y,
n]
consider f being
Function such that A11:
dom f = succ x
and A12:
for
y being
object st
y in succ x holds
ex
n being
Nat st
(
f . y = n &
S2[
y,
n] & ( for
m being
Nat st
S2[
y,
m] holds
n <= m ) )
from TREES_2:sch 4(A7);
consider k being
Nat such that A13:
for
m being
Nat st
m in rng f holds
m <= k
by A6, A11, Lm1, FINSET_1:8;
consider B being
Branch of
T such that A14:
x in B
and A15:
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 A16:
p in B
and A17:
len p >= (len x) + (k + 1)
by A15;
reconsider r =
p | (Seg ((len x) + 1)) as
FinSequence of
NAT by FINSEQ_1:18;
(len x) + 1
<= ((len x) + 1) + k
by NAT_1:11;
then A18:
len p >= (len x) + 1
by A17, XXREAL_0:2;
A19:
r is_a_prefix_of p
;
A20:
len r = (len x) + 1
by A18, FINSEQ_1:17;
A21:
r in B
by A16, A19, Th25;
then
x is_a_prefix_of r
by A14, A20, Th27, NAT_1:11;
then consider j being
FinSequence such that A22:
r = x ^ j
by TREES_1:1;
(len x) + (len j) = len r
by A22, FINSEQ_1:22;
then A23:
j = <*(j . 1)*>
by A20, FINSEQ_1:40;
A24:
(
dom r = Seg (len r) & 1
<= 1
+ (len x) )
by FINSEQ_1:def 3, NAT_1:11;
(len x) + 1
<= len r
by A18, FINSEQ_1:17;
then
(
(x ^ <*(j . 1)*>) . ((len x) + 1) = j . 1 &
(len x) + 1
in dom r )
by A24, FINSEQ_1:1, FINSEQ_1:42;
then
j . 1
in rng r
by A22, A23, FUNCT_1:def 3;
then reconsider l =
j . 1 as
Nat ;
A25:
x ^ <*l*> in succ x
by A21, A22, A23;
then consider n being
Nat such that A26:
f . (x ^ <*l*>) = n
and A27:
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
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 A12;
n in rng f
by A11, A25, A26, FUNCT_1:def 3;
then
n <= k
by A13;
then
(len r) + n <= ((len x) + 1) + k
by A20, XREAL_1:7;
hence
contradiction
by A16, A17, A21, A22, A23, A27, XXREAL_0:2;
verum
end;
reconsider e = {} as Element of T by TREES_1:22;
A28:
S1[e]
defpred S2[ object ] means ex t being Element of T st
( t = $1 & S1[t] );
defpred S3[ object , object ] means ex p being FinSequence of NAT ex n being Nat st
( $1 = p & p ^ <*n*> in T & $2 = p ^ <*n*> );
A33:
( e in T & S2[e] )
by A28;
A34:
for x being object st x in T & S2[x] holds
ex y being object st
( y in T & S3[x,y] & S2[y] )
proof
let x be
object ;
( x in T & S2[x] implies ex y being object st
( y in T & S3[x,y] & S2[y] ) )
assume
x in T
;
( not S2[x] or ex y being object st
( y in T & S3[x,y] & S2[y] ) )
given t being
Element of
T such that A35:
t = x
and A36:
S1[
t]
;
ex y being object st
( y in T & S3[x,y] & S2[y] )
consider n being
Nat such that A37:
t ^ <*n*> in T
and A38:
S1[
t ^ <*n*>]
by A3, A36;
reconsider y =
t ^ <*n*> as
set ;
take
y
;
( y in T & S3[x,y] & S2[y] )
thus
(
y in T &
S3[
x,
y] )
by A35, A37;
S2[y]
reconsider t1 =
t ^ <*n*> as
Element of
T by A37;
take
t1
;
( t1 = y & S1[t1] )
thus
(
t1 = y &
S1[
t1] )
by A38;
verum
end;
ex f being Function st
( dom f = NAT & rng f c= T & f . 0 = e & ( for k being Nat holds
( S3[f . k,f . (k + 1)] & S2[f . k] ) ) )
from TREES_2:sch 5(A33, A34);
then consider f being Function such that
A39:
dom f = NAT
and
A40:
rng f c= T
and
A41:
f . 0 = e
and
A42:
for k being Nat holds
( ex p being FinSequence of NAT ex n being 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] ) )
;
reconsider C = rng f as Subset of T by A40;
A43:
now for k, n being Nat holds S4[n]end;
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 A53:
p in C
and A54:
q in C
;
p,q are_c=-comparable
consider x being
object such that A55:
x in NAT
and A56:
p = f . x
by A39, A53, FUNCT_1:def 3;
consider y being
object such that A57:
y in NAT
and A58:
q = f . y
by A39, A54, FUNCT_1:def 3;
reconsider x =
x,
y =
y as
Nat by A55, A57;
(
x <= y or
y <= x )
;
hence
(
p is_a_prefix_of q or
q is_a_prefix_of p )
by A52, A56, A58;
XBOOLE_0:def 9 verum
end;
then reconsider C = C as Chain of T ;
take
C
; not C is finite
defpred S4[ Nat] means for p being FinSequence of NAT st p = f . $1 holds
len p = $1;
A59:
S4[ 0 ]
by A41;
A60:
for k being Nat st S4[k] holds
S4[k + 1]
A65:
for k being Nat holds S4[k]
from NAT_1:sch 2(A59, A60);
f is one-to-one
then
NAT ,C are_equipotent
by A39, WELLORD2:def 4;
hence
not C is finite
by CARD_1:38; verum