Seg n is finite

proof

A1: n = { k where k is Element of NAT : k < n } by AXIOMS:30;
A3: for x being set st x in n holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in n implies ex y being set st S₁[x,y] )
assume x in n ; :: thesis: ex y being set st S₁[x,y]
then ex k being Element of NAT st
( x = k & k < n ) by A1;
then reconsider k = x as Nat ;
take k + 1 ; :: thesis: S₁[x,k + 1]
thus S₁[x,k + 1] ; :: thesis: verum

end;

consider f being Function such that
A4: dom f = n and
A5: for x being set st x in n holds
S₁[x,f . x] from CLASSES1:sch 1(A3);
take f ; :: according to FINSET_1:def 1 :: thesis: ( rng f = Seg n & dom f in omega )
thus rng f = Seg n :: thesis: dom f in omega

proof

thus rng f c= Seg n :: according to XBOOLE_0:def 10 :: thesis: Seg n c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Seg n )
assume x in rng f ; :: thesis: x in Seg n
then consider y being set such that
A6: y in dom f and
A7: x = f . y by FUNCT_1:def 5;
consider k being Nat such that
A8: y = k and
A9: x = k + 1 by A4, A5, A6, A7;
A10: 1 <= k + 1 by NAT_1:11;
ex m being Element of NAT st
( m = y & m < n ) by A1, A4, A6;
then k + 1 <= n by A8, NAT_1:13;
hence x in Seg n by A9, A10; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg n or x in rng f )
assume x in Seg n ; :: thesis: x in rng f
then consider k being Element of NAT such that
A11: x = k and
A12: 1 <= k and
A13: k <= n ;
consider i being Nat such that
A14: 1 + i = k by A12, NAT_1:10;
A15: i in NAT by ORDINAL1:def 13;
i < n by A13, A14, NAT_1:13;
then A16: i in n by A1, A15;
then S₁[i,f . i] by A5;
hence x in rng f by A4, A11, A14, A16, FUNCT_1:def 5; :: thesis: verum

end;

thus dom f in omega by A4, ORDINAL1:def 13; :: thesis: verum

end;

hence Seg n is finite ; :: thesis: verum