let X be set ; :: thesis: for A being Ordinal
for U being Grothendieck st X in U & X,A are_equipotent holds
A in U
let A be Ordinal; :: thesis: for U being Grothendieck st X in U & X,A are_equipotent holds
A in U
let U be Grothendieck; :: thesis: ( X in U & X,A are_equipotent implies A in U )
defpred S₁[ Ordinal] means for X being set st X,$1 are_equipotent & X in U holds
$1 in U;
A1: for A being Ordinal st ( for C being Ordinal st C in A holds
S₁[C] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds
S₁[C] ) implies S₁[A] )
assume A2: for C being Ordinal st C in A holds
S₁[C] ; :: thesis: S₁[A]
let S be set ; :: thesis: ( S,A are_equipotent & S in U implies A in U )
assume A3: ( S,A are_equipotent & S in U ) ; :: thesis: A in U
consider f being Function such that
A4: ( f is one-to-one & dom f = S & rng f = A ) by A3, WELLORD2:def 4;
rng f c= U

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in U )
assume A5: y in rng f ; :: thesis: y in U
reconsider B = y as Ordinal by A5, A4;
A6: B |` f is one-to-one by A4, FUNCT_1:58;
A7: rng (B |` f) = B by A4, RELAT_1:89, A5, ORDINAL1:def 2;
dom (B |` f) in U by A3, A4, CLASSES1:def 1, RELAT_1:186;
hence y in U by A7, A6, WELLORD2:def 4, A5, A4, A2; :: thesis: verum

end;

hence A in U by A4, A3, Th2; :: thesis: verum

end;

for O being Ordinal holds S₁[O] from ORDINAL1:sch 2(A1);
hence ( X in U & X,A are_equipotent implies A in U ) ; :: thesis: verum