let T be Tree; :: thesis: ( ( 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
; :: thesis: 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;
:: thesis: ( 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*>]
;
:: thesis: 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 A10:
dom f = succ x
and A11:
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);
rng f is
finite
by A6, A10, FINSET_1:26;
then consider k being
Element of
NAT such that A12:
for
m being
Element of
NAT st
m in rng f holds
m <= k
by Lm1;
consider B being
Branch of
T such that A13:
(
x in B & 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 A14:
(
p in B &
len p >= (len x) + (k + 1) )
by A13;
reconsider r =
p | (Seg ((len x) + 1)) as
FinSequence of
NAT by FINSEQ_1:23;
(
(len x) + 1
<= ((len x) + 1) + k &
((len x) + 1) + k = (len x) + (1 + k) & 1
+ k = k + 1 )
by NAT_1:11;
then A15:
len p >= (len x) + 1
by A14, XXREAL_0:2;
then A16:
(
r is_a_prefix_of p &
len r = (len x) + 1 )
by FINSEQ_1:21, TREES_1:def 1;
then A17:
(
r in B &
len x <= len r )
by A14, Th27, NAT_1:11;
then
x is_a_prefix_of r
by A13, Th29;
then consider j being
FinSequence such that A18:
r = x ^ j
by TREES_1:8;
(len x) + (len j) = len r
by A18, FINSEQ_1:35;
then A19:
(
j = <*(j . 1)*> &
(x ^ <*(j . 1)*>) . ((len x) + 1) = j . 1 )
by A16, FINSEQ_1:57, FINSEQ_1:59;
A20:
dom r = Seg (len r)
by FINSEQ_1:def 3;
( 1
<= 1
+ (len x) & 1
+ (len x) = (len x) + 1 &
(len x) + 1
<= len r )
by A15, FINSEQ_1:21, NAT_1:11;
then
(len x) + 1
in dom r
by A20, FINSEQ_1:3;
then
(
j . 1
in rng r &
rng r c= NAT )
by A18, A19, FUNCT_1:def 5;
then reconsider l =
j . 1 as
Element of
NAT ;
A21:
x ^ <*l*> in succ x
by A17, A18, A19;
then consider n being
Element of
NAT such that A22:
(
f . (x ^ <*l*>) = n & ( 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 ) & ( 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 A11;
A23:
(len r) + n > len p
by A14, A17, A18, A19, A22;
n in rng f
by A10, A21, A22, FUNCT_1:def 5;
then
n <= k
by A12;
then
(
(len r) + n <= ((len x) + 1) + k &
((len x) + 1) + k = (len x) + (1 + k) & 1
+ k = k + 1 )
by A16, XREAL_1:9;
hence
contradiction
by A14, A23, XXREAL_0:2;
:: thesis: verum
end;
reconsider e = {} as Element of T by TREES_1:47;
A24:
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*> );
A29:
( e in T & S2[e] )
by A24;
A30:
for x being set st x in T & S2[x] holds
ex y being set st
( y in T & S3[x,y] & S2[y] )
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(A29, A30);
then consider f being Function such that
A33:
( dom f = NAT & rng f c= T & f . 0 = e )
and
A34:
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] ) )
;
reconsider C = rng f as Subset of T by A33;
C is Chain of T
proof
let p be
FinSequence of
NAT ;
:: according to TREES_2:def 3 :: thesis: 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 ;
:: thesis: ( p in C & q in C implies p,q are_c=-comparable )
assume A43:
(
p in C &
q in C )
;
:: thesis: p,q are_c=-comparable
then consider x being
set such that A44:
(
x in NAT &
p = f . x )
by A33, FUNCT_1:def 5;
consider y being
set such that A45:
(
y in NAT &
q = f . y )
by A33, A43, FUNCT_1:def 5;
reconsider x =
x,
y =
y as
Element of
NAT by A44, A45;
(
x <= y or
y <= x )
;
hence
(
p is_a_prefix_of q or
q is_a_prefix_of p )
by A41, A44, A45;
:: according to XBOOLE_0:def 9 :: thesis: verum
end;
then reconsider C = C as Chain of T ;
take
C
; :: thesis: not C is finite
defpred S4[ Element of NAT ] means for p being FinSequence of NAT st p = f . $1 holds
len p = $1;
A46:
S4[ 0 ]
by A33;
A47:
for k being Element of NAT st S4[k] holds
S4[k + 1]
A51:
for k being Element of NAT holds S4[k]
from NAT_1:sch 1(A46, A47);
f is one-to-one
then
NAT ,C are_equipotent
by A33, WELLORD2:def 4;
hence
not C is finite
by CARD_1:68; :: thesis: verum