let n be Element of NAT ; width (elementary_tree (n + 1)) = n + 1
set T = elementary_tree (n + 1);
A1:
now A2:
{ <*k*> where k is Element of NAT : k < n + 1 } is
AntiChain_of_Prefixes-like
reconsider X =
{ <*k*> where k is Element of NAT : k < n + 1 } as
AntiChain_of_Prefixes by A2;
A7:
X c= elementary_tree (n + 1)
by XBOOLE_1:7;
reconsider X =
X as
AntiChain_of_Prefixes of
elementary_tree (n + 1) by A7, Def14;
take X =
X;
( n + 1 = card X & ( for Y being AntiChain_of_Prefixes of elementary_tree (n + 1) holds card Y <= card X ) )A8:
X,
Seg (n + 1) are_equipotent
proof
defpred S1[
set ,
set ]
means ex
n being
Element of
NAT st
( $1
= <*n*> & $2
= n + 1 );
A9:
for
x,
y,
z being
set st
x in X &
S1[
x,
y] &
S1[
x,
z] holds
y = z
proof
let x,
y,
z be
set ;
( x in X & S1[x,y] & S1[x,z] implies y = z )
assume
x in X
;
( not S1[x,y] or not S1[x,z] or y = z )
given n1 being
Element of
NAT such that A10:
(
x = <*n1*> &
y = n1 + 1 )
;
( not S1[x,z] or y = z )
given n2 being
Element of
NAT such that A11:
(
x = <*n2*> &
z = n2 + 1 )
;
y = z
A12:
<*n1*> . 1
= n1
by FINSEQ_1:def 8;
thus
y = z
by A10, A11, A12, FINSEQ_1:def 8;
verum
end;
A13:
for
x being
set st
x in X holds
ex
y being
set st
S1[
x,
y]
proof
let x be
set ;
( x in X implies ex y being set st S1[x,y] )
assume A14:
x in X
;
ex y being set st S1[x,y]
consider k being
Element of
NAT such that A15:
x = <*k*>
and
k < n + 1
by A14;
reconsider y =
k + 1 as
set ;
take
y
;
S1[x,y]
thus
S1[
x,
y]
by A15;
verum
end;
consider f being
Function such that A16:
(
dom f = X & ( for
x being
set st
x in X holds
S1[
x,
f . x] ) )
from CLASSES1:sch 1(A13);
take
f
;
WELLORD2:def 4 ( f is one-to-one & proj1 f = X & proj2 f = Seg (n + 1) )
thus
f is
one-to-one
( proj1 f = X & proj2 f = Seg (n + 1) )
thus
dom f = X
by A16;
proj2 f = Seg (n + 1)
thus
rng f c= Seg (n + 1)
XBOOLE_0:def 10 Seg (n + 1) is_a_prefix_of proj2 f
let x be
set ;
TARSKI:def 3 ( not x in Seg (n + 1) or x in proj2 f )
assume A28:
x in Seg (n + 1)
;
x in proj2 f
reconsider k =
x as
Element of
NAT by A28;
A29:
1
<= k
by A28, FINSEQ_1:3;
A30:
k <= n + 1
by A28, FINSEQ_1:3;
consider m being
Nat such that A31:
k = 1
+ m
by A29, NAT_1:10;
reconsider m =
m as
Element of
NAT by ORDINAL1:def 13;
A32:
m < n + 1
by A30, A31, NAT_1:13;
A33:
<*m*> in X
by A32;
A34:
S1[
<*m*>,
f . <*m*>]
by A16, A33;
A35:
x = f . <*m*>
by A9, A31, A33, A34;
thus
x in proj2 f
by A16, A33, A35, FUNCT_1:def 5;
verum
end; A36:
card (Seg (n + 1)) = card X
by A8, CARD_1:21;
thus
n + 1
= card X
by A36, FINSEQ_1:78;
for Y being AntiChain_of_Prefixes of elementary_tree (n + 1) holds card Y <= card Xlet Y be
AntiChain_of_Prefixes of
elementary_tree (n + 1);
card Y <= card XA37:
Y c= elementary_tree (n + 1)
by Def14;
A38:
(
{} in Y implies
Y = {{} } )
proof
assume that A39:
{} in Y
and A40:
Y <> {{} }
;
contradiction
consider x being
set such that A41:
( (
x in Y & not
x in {{} } ) or (
x in {{} } & not
x in Y ) )
by A40, TARSKI:2;
A42:
{} <> x
by A39, A41, TARSKI:def 1;
reconsider x =
x as
FinSequence of
NAT by A37, A39, A41, Th44, TARSKI:def 1;
A43:
{} is_a_prefix_of x
by XBOOLE_1:2;
A44:
{} ,
x are_c=-comparable
by A43, XBOOLE_0:def 9;
thus
contradiction
by A39, A41, A42, A44, Def13, TARSKI:def 1;
verum
end; A45:
(
card {{} } = 1 & 1
<= 1
+ n )
by CARD_1:50, NAT_1:11;
thus
card Y <= card X
by A36, A38, A45, A46, FINSEQ_1:78;
verum end;
thus
width (elementary_tree (n + 1)) = n + 1
by A1, Def16; verum