Description: Lemma for transfinite recursion. Assuming ax-rep ,
dom recs e.V <-> recs e. V , so since dom recs is an ordinal,
it must be equal to On . (Contributed by NM, 14-Aug-1994)(Revised by Mario Carneiro, 9-May-2015)

Ref

Expression

Hypothesis

tfrlem.1

|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }