let n be Nat; width (elementary_tree (n + 1)) = n + 1
set T = elementary_tree (n + 1);
now ex X being AntiChain_of_Prefixes of elementary_tree (n + 1) st
( n + 1 = card X & ( for Y being AntiChain_of_Prefixes of elementary_tree (n + 1) holds card Y <= card X ) )
{ <*k*> where k is Nat : k < n + 1 } is
AntiChain_of_Prefixes-like
then reconsider X =
{ <*k*> where k is Nat : k < n + 1 } as
AntiChain_of_Prefixes ;
X c= elementary_tree (n + 1)
by XBOOLE_1:7;
then reconsider X =
X as
AntiChain_of_Prefixes of
elementary_tree (n + 1) by Def11;
take X =
X;
( n + 1 = card X & ( for Y being AntiChain_of_Prefixes of elementary_tree (n + 1) holds card Y <= card X ) )
X,
Seg (n + 1) are_equipotent
proof
defpred S1[
object ,
object ]
means ex
n being
Nat st
( $1
= <*n*> & $2
= n + 1 );
A1:
for
x,
y,
z being
set st
x in X &
S1[
x,
y] &
S1[
x,
z] holds
y = z
A4:
for
x being
object st
x in X holds
ex
y being
object st
S1[
x,
y]
proof
let x be
object ;
( x in X implies ex y being object st S1[x,y] )
assume
x in X
;
ex y being object st S1[x,y]
then consider k being
Nat such that A5:
x = <*k*>
and
k < n + 1
;
reconsider y =
k + 1 as
set ;
take
y
;
S1[x,y]
thus
S1[
x,
y]
by A5;
verum
end;
consider f being
Function such that A6:
(
dom f = X & ( for
x being
object st
x in X holds
S1[
x,
f . x] ) )
from CLASSES1:sch 1(A4);
take
f
;
WELLORD2:def 4 ( f is one-to-one & dom f = X & rng f = Seg (n + 1) )
thus
f is
one-to-one
( dom f = X & rng f = Seg (n + 1) )
thus
dom f = X
by A6;
rng f = Seg (n + 1)
thus
rng f c= Seg (n + 1)
XBOOLE_0:def 10 Seg (n + 1) is_a_prefix_of rng f
let x be
object ;
TARSKI:def 3 ( not x in Seg (n + 1) or x in rng f )
assume A14:
x in Seg (n + 1)
;
x in rng f
then reconsider k =
x as
Nat ;
A15:
1
<= k
by A14, FINSEQ_1:1;
A16:
k <= n + 1
by A14, FINSEQ_1:1;
consider m being
Nat such that A17:
k = 1
+ m
by A15, NAT_1:10;
reconsider m =
m as
Nat ;
m < n + 1
by A16, A17, NAT_1:13;
then A18:
<*m*> in X
;
then
S1[
<*m*>,
f . <*m*>]
by A6;
then
x = f . <*m*>
by A1, A17, A18;
hence
x in rng f
by A6, A18, FUNCT_1:def 3;
verum
end; then A19:
card (Seg (n + 1)) = card X
by CARD_1:5;
hence
n + 1
= card X
by FINSEQ_1:57;
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 XA20:
Y c= elementary_tree (n + 1)
by Def11;
A21:
(
{} in Y implies
Y = {{}} )
proof
assume that A22:
{} in Y
and A23:
Y <> {{}}
;
contradiction
consider x being
object such that A24:
( (
x in Y & not
x in {{}} ) or (
x in {{}} & not
x in Y ) )
by A23, TARSKI:2;
A25:
{} <> x
by A22, A24, TARSKI:def 1;
reconsider x =
x as
FinSequence of
NAT by A20, A24, Th18;
{} is_a_prefix_of x
;
then
{} ,
x are_c=-comparable
;
hence
contradiction
by A22, A24, A25, Def10, TARSKI:def 1;
verum
end; A26:
(
card {{}} = 1 & 1
<= 1
+ n )
by CARD_1:30, NAT_1:11;
hence
card Y <= card X
by A19, A21, A26, FINSEQ_1:57;
verum end;
hence
width (elementary_tree (n + 1)) = n + 1
by Def13; verum