defpred S1[ Ordinal] means for X being set st X in Rank $1 holds
not X, Rank $1 are_equipotent ;
A1:
for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be
Ordinal;
( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A2:
for
B being
Ordinal st
B in A holds
S1[
B]
;
S1[A]
let X be
set ;
( X in Rank A implies not X, Rank A are_equipotent )
assume A3:
X in Rank A
;
not X, Rank A are_equipotent
A4:
now ( ex B being Ordinal st A = succ B implies not X, Rank A are_equipotent )given B being
Ordinal such that A5:
A = succ B
;
not X, Rank A are_equipotent A6:
B c= A
by A5, ORDINAL1:6, ORDINAL1:def 2;
A7:
Rank (succ B) = bool (Rank B)
by Lm2;
then A8:
not
Rank B,
Rank A are_equipotent
by A5, CARD_1:13;
Rank B c= Rank A
by A6, Th37;
hence
not
X,
Rank A are_equipotent
by A3, A5, A7, A8, CARD_1:24;
verum end;
now ( A <> {} & ( for B being Ordinal holds A <> succ B ) implies not X, Rank A are_equipotent )assume that A9:
A <> {}
and A10:
for
B being
Ordinal holds
A <> succ B
;
not X, Rank A are_equipotent
A is
limit_ordinal
by A10, ORDINAL1:29;
then consider B being
Ordinal such that A11:
B in A
and A12:
X in Rank B
by A3, A9, Th31;
A13:
( not
X,
Rank B are_equipotent &
X c= Rank B )
by A2, A11, A12, ORDINAL1:def 2;
Rank B c= Rank A
by A11, Th36, ORDINAL1:def 2;
hence
not
X,
Rank A are_equipotent
by A13, CARD_1:24;
verum end;
hence
not
X,
Rank A are_equipotent
by A3, A4, Lm2;
verum
end;
A14:
for A being Ordinal holds S1[A]
from ORDINAL1:sch 2(A1);
let A be Ordinal; for X being set st X in Rank A holds
( not X, Rank A are_equipotent & card X in card (Rank A) )
let X be set ; ( X in Rank A implies ( not X, Rank A are_equipotent & card X in card (Rank A) ) )
assume A15:
X in Rank A
; ( not X, Rank A are_equipotent & card X in card (Rank A) )
A16:
card X c= card (Rank A)
by A15, CARD_1:11, ORDINAL1:def 2;
card X <> card (Rank A)
by A14, A15, CARD_1:5;
hence
( not X, Rank A are_equipotent & card X in card (Rank A) )
by A14, A15, A16, CARD_1:3; verum