let U be Grothendieck; :: thesis: for X being set st X c= U & not X in U holds
ex f being Function st
( f is one-to-one & dom f = On U & rng f = X )
let X be set ; :: thesis: ( X c= U & not X in U implies ex f being Function st
( f is one-to-one & dom f = On U & rng f = X ) )
assume A1: ( X c= U & not X in U ) ; :: thesis: ex f being Function st
( f is one-to-one & dom f = On U & rng f = X )
for x being set st x in On U holds
( x is Ordinal & x c= On U )

proof

let x be set ; :: thesis: ( x in On U implies ( x is Ordinal & x c= On U ) )
assume A2: x in On U ; :: thesis: ( x is Ordinal & x c= On U )
then ( x in U & x is Ordinal ) by ORDINAL1:def 9;
then x c= U by ORDINAL1:def 2;
hence ( x is Ordinal & x c= On U ) by A2, ORDINAL1:def 9; :: thesis: verum

end;

then ( On U is epsilon-transitive & On U is epsilon-connected ) by ORDINAL1:19;
then reconsider Lambda = On U as Ordinal ;
ex THE being Function st
for x being set st {} <> x & x c= X holds
THE . x in x

proof

consider V being Relation such that
A3: V well_orders X by WELLORD2:17;
defpred S₁[ object , object ] means for A being set st A = $1 holds
( $2 in A & ( for b being object st b in A holds
[$2,b] in V ) );
A4: for x being object st x in (bool X) \ {{}} holds
ex u being object st S₁[x,u]

proof

let x be object ; :: thesis: ( x in (bool X) \ {{}} implies ex u being object st S₁[x,u] )
assume A5: x in (bool X) \ {{}} ; :: thesis: ex u being object st S₁[x,u]
reconsider y = x as set by TARSKI:1;
consider a being object such that
A6: a in y and
A7: for b being object st b in y holds
[a,b] in V by A3, WELLORD1:5, A5, ZFMISC_1:56;
take a ; :: thesis: S₁[x,a]
thus S₁[x,a] by A6, A7; :: thesis: verum

end;

consider THE being Function such that
dom THE = (bool X) \ {{}} and
A8: for e being object st e in (bool X) \ {{}} holds
S₁[e,THE . e] from CLASSES1:sch 1(A4);
take THE ; :: thesis: for x being set st {} <> x & x c= X holds
THE . x in x
let x be set ; :: thesis: ( {} <> x & x c= X implies THE . x in x )
assume ( {} <> x & x c= X ) ; :: thesis: THE . x in x
then x in (bool X) \ {{}} by ZFMISC_1:56;
hence THE . x in x by A8; :: thesis: verum

end;

then consider THE being Function such that
A9: for x being set st {} <> x & x c= X holds
THE . x in x ;
deffunc H₁( set ) -> set = { (the_rank_of x) where x is Element of $1 : x in $1 } ;
A10: for A being set
for x being object holds
( x in H₁(A) iff ex a being set st
( a in A & x = the_rank_of a ) )

proof

let A be set ; :: thesis: for x being object holds
( x in H₁(A) iff ex a being set st
( a in A & x = the_rank_of a ) )
let x be object ; :: thesis: ( x in H₁(A) iff ex a being set st
( a in A & x = the_rank_of a ) )
thus ( x in H₁(A) implies ex a being set st
( a in A & x = the_rank_of a ) ) :: thesis: ( ex a being set st
( a in A & x = the_rank_of a ) implies x in H₁(A) )

proof

assume x in H₁(A) ; :: thesis: ex a being set st
( a in A & x = the_rank_of a )
then consider a being Element of A such that
A11: ( x = the_rank_of a & a in A ) ;
take a ; :: thesis: ( a in A & x = the_rank_of a )
thus ( a in A & x = the_rank_of a ) by A11; :: thesis: verum

end;

assume ex a being set st
( a in A & x = the_rank_of a ) ; :: thesis: x in H₁(A)
hence x in H₁(A) ; :: thesis: verum

end;

defpred S₁[ set , object ] means ( $2 in X \ $1 & ( for B being Ordinal st B in H₁(X \ $1) holds
the_rank_of $2 c= B ) );
deffunc H₂( Sequence) -> set = THE . { x where x is Element of X : S₁[ rng $1,x] } ;
consider f being Sequence such that
A12: dom f = Lambda and
A13: for A being Ordinal
for L being Sequence st A in Lambda & L = f | A holds
f . A = H₂(L) from ORDINAL1:sch 4();
A14: for A being Ordinal st A in Lambda holds
S₁[ rng (f | A),f . A]

proof

let A be Ordinal; :: thesis: ( A in Lambda implies S₁[ rng (f | A),f . A] )
assume A15: A in Lambda ; :: thesis: S₁[ rng (f | A),f . A]
A16: A in U by A15, ORDINAL1:def 9;
A17: dom (f | A) = A by A12, RELAT_1:62, A15, ORDINAL1:def 2;
A18: f . A = H₂(f | A) by A15, A13;
set II = { x where x is Element of X : S₁[ rng (f | A),x] } ;
{ x where x is Element of X : S₁[ rng (f | A),x] } c= X

proof

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in { x where x is Element of X : S₁[ rng (f | A),x] } or i in X )
assume i in { x where x is Element of X : S₁[ rng (f | A),x] } ; :: thesis: i in X
then ex x being Element of X st
( i = x & S₁[ rng (f | A),x] ) ;
hence i in X ; :: thesis: verum

end;

then reconsider II = { x where x is Element of X : S₁[ rng (f | A),x] } as Subset of X ;
defpred S₂[ Ordinal] means ex a being set st
( a in X \ (rng (f | A)) & $1 = the_rank_of a );
A19: ex O being Ordinal st S₂[O]

proof

assume A20: for O being Ordinal holds not S₂[O] ; :: thesis: contradiction
A21: X \ (rng (f | A)) = {}

proof

assume X \ (rng (f | A)) <> {} ; :: thesis: contradiction
then consider a being object such that
A22: a in X \ (rng (f | A)) by XBOOLE_0:def 1;
S₂[ the_rank_of a] by A22;
hence contradiction by A20; :: thesis: verum

end;

A23: dom (X |` (f | A)) in U by A17, A16, CLASSES1:def 1, FUNCT_1:56;
rng (X |` (f | A)) = X by A21, XBOOLE_1:37, RELAT_1:89;
hence contradiction by A1, Th2, A23; :: thesis: verum

end;

consider Min being Ordinal such that
A24: ( S₂[Min] & ( for O being Ordinal st S₂[O] holds
Min c= O ) ) from ORDINAL1:sch 1(A19);
consider t being set such that
A25: ( t in X \ (rng (f | A)) & Min = the_rank_of t ) by A24;
for B being Ordinal st B in H₁(X \ (rng (f | A))) holds
the_rank_of t c= B

proof

let B be Ordinal; :: thesis: ( B in H₁(X \ (rng (f | A))) implies the_rank_of t c= B )
assume A26: B in H₁(X \ (rng (f | A))) ; :: thesis: the_rank_of t c= B
ex a being set st
( a in X \ (rng (f | A)) & B = the_rank_of a ) by A10, A26;
hence the_rank_of t c= B by A24, A25; :: thesis: verum

end;

then t in II by A25;
then THE . II in II by A9;
then ex x being Element of X st
( x = THE . II & S₁[ rng (f | A),x] ) ;
hence S₁[ rng (f | A),f . A] by A18; :: thesis: verum

end;

A27: f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume A28: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
assume A29: x1 <> x2 ; :: thesis: contradiction
reconsider x1 = x1, x2 = x2 as Ordinal by A28;
A30: ( f . x1 in X \ (rng (f | x1)) & f . x2 in X \ (rng (f | x2)) ) by A14, A28, A12;

per cases ( x1 in x2 or x2 in x1 ) by A28, ORDINAL1:def 3, A29;

suppose x1 in x2 ; :: thesis: contradiction

then ( x1 in dom (f | x2) & f . x1 = (f | x2) . x1 ) by A28, RELAT_1:57, FUNCT_1:49;
then f . x1 in rng (f | x2) by FUNCT_1:def 3;
hence contradiction by A30, XBOOLE_0:def 5, A28; :: thesis: verum

end;

suppose x2 in x1 ; :: thesis: contradiction

then ( x2 in dom (f | x1) & f . x2 = (f | x1) . x2 ) by A28, RELAT_1:57, FUNCT_1:49;
then f . x2 in rng (f | x1) by FUNCT_1:def 3;
hence contradiction by A30, XBOOLE_0:def 5, A28; :: thesis: verum

end;

end;

end;

A31: rng f c= X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in X )
assume A32: y in rng f ; :: thesis: y in X
consider A being object such that
A33: ( A in dom f & f . A = y ) by A32, FUNCT_1:def 3;
reconsider A = A as Ordinal by A33;
S₁[ rng (f | A),f . A] by A12, A14, A33;
hence y in X by A33; :: thesis: verum

end;

A34: X c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in rng f )
assume A35: x in X ; :: thesis: x in rng f
assume A36: not x in rng f ; :: thesis: contradiction
Rrank x in U by A1, A35, Th14;
then A37: bool (Rrank x) in U by Def1;
rng f c= bool (Rrank x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in bool (Rrank x) )
assume A38: y in rng f ; :: thesis: y in bool (Rrank x)
consider A being object such that
A39: ( A in dom f & f . A = y ) by A38, FUNCT_1:def 3;
reconsider A = A as Ordinal by A39;
rng (f | A) c= rng f by RELAT_1:70;
then not x in rng (f | A) by A36;
then x in X \ (rng (f | A)) by A35, XBOOLE_0:def 5;
then the_rank_of x in H₁(X \ (rng (f | A))) ;
then the_rank_of (f . A) in succ (the_rank_of x) by A39, A12, A14, ORDINAL1:22;
then A40: Rank (succ (the_rank_of (f . A))) c= Rank (succ (the_rank_of x)) by CLASSES1:37, ORDINAL1:21;
f . A in Rank (succ (the_rank_of (f . A))) by CLASSES1:def 8;
then f . A in Rank (succ (the_rank_of x)) by A40;
hence y in bool (Rrank x) by A39, CLASSES1:30; :: thesis: verum

end;

then A41: rng f in U by A37, CLASSES1:def 1;
A42: ( rng (f ") = dom f & dom (f ") = rng f ) by A27, FUNCT_1:33;
dom f in U by A42, A41, A12, ORDINAL2:7, Th2;
then dom f in Lambda by ORDINAL1:def 9;
hence contradiction by A12; :: thesis: verum

end;

take f ; :: thesis: ( f is one-to-one & dom f = On U & rng f = X )
thus ( f is one-to-one & dom f = On U & rng f = X ) by A34, A31, A27, A12; :: thesis: verum