[FOM] Replacement

[Jan Pax]

>    >  Exactly, I have the same thing to point here: can the existence of
>    >  Hartogs function proved without Replacement?
>    >  

If we have a well ordered set W then h(W) is an ordinal whose initial segment is isomorphic to W.
By my previous post this requires replacement.

>    
>    >  Another thing:
>    >  Consider the statement: If F: On --> P(S) be an increasing function,
>    >  where P(S) is the power set of non-empty S; then f(a) = f(a+) for some
>    >  ordinal a.
>    >  Can the above proved without Replacement? Or is there a counterexample
>    >  in ZF - Replacement ?
> 

Take union of  {  F(alpha) \  alpha < | P(S) |  }. 
Some element from the preimage of this union and its successor will be the required a and a+. 
Replacement is not needed.