let U be Grothendieck; 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 ; ( 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 )
; 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 )
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
then consider THE being Function such that
A9:
for x being set st {} <> x & x c= X holds
THE . x in x
;
deffunc H1( 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 H1(A) iff ex a being set st
( a in A & x = the_rank_of a ) )
defpred S1[ set , object ] means ( $2 in X \ $1 & ( for B being Ordinal st B in H1(X \ $1) holds
the_rank_of $2 c= B ) );
deffunc H2( Sequence) -> set = THE . { x where x is Element of X : S1[ 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 = H2(L)
from ORDINAL1:sch 4();
A14:
for A being Ordinal st A in Lambda holds
S1[ rng (f | A),f . A]
proof
let A be
Ordinal;
( A in Lambda implies S1[ rng (f | A),f . A] )
assume A15:
A in Lambda
;
S1[ 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 = H2(
f | A)
by A15, A13;
set II =
{ x where x is Element of X : S1[ rng (f | A),x] } ;
{ x where x is Element of X : S1[ rng (f | A),x] } c= X
then reconsider II =
{ x where x is Element of X : S1[ rng (f | A),x] } as
Subset of
X ;
defpred S2[
Ordinal]
means ex
a being
set st
(
a in X \ (rng (f | A)) & $1
= the_rank_of a );
A19:
ex
O being
Ordinal st
S2[
O]
consider Min being
Ordinal such that A24:
(
S2[
Min] & ( for
O being
Ordinal st
S2[
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 H1(
X \ (rng (f | A))) holds
the_rank_of t c= B
then
t in II
by A25;
then
THE . II in II
by A9;
then
ex
x being
Element of
X st
(
x = THE . II &
S1[
rng (f | A),
x] )
;
hence
S1[
rng (f | A),
f . A]
by A18;
verum
end;
A27:
f is one-to-one
A31:
rng f c= X
A34:
X c= rng f
take
f
; ( 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; verum