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_{1}[ 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_{1}[C] ) holds

S_{1}[A]
_{1}[O]
from ORDINAL1:sch 2(A1);

hence ( X in U & X,A are_equipotent implies A in U ) ; :: thesis: verum

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

$1 in U;

A1: for A being Ordinal st ( for C being Ordinal st C in A holds

S

S

proof

for O being Ordinal holds S
let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds

S_{1}[C] ) implies S_{1}[A] )

assume A2: for C being Ordinal st C in A holds

S_{1}[C]
; :: thesis: S_{1}[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

end;S

assume A2: for C being Ordinal st C in A holds

S

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

hence
A in U
by A4, A3, Th2; :: thesis: verum
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;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

hence ( X in U & X,A are_equipotent implies A in U ) ; :: thesis: verum