# Metamath Proof Explorer

## Theorem tfrlem14

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 ) ) ) }
Assertion tfrlem14
|- dom recs ( F ) = On

### Proof

Step Hyp Ref Expression
1 tfrlem.1
|-  A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
2 1 tfrlem13
|-  -. recs ( F ) e. _V
3 1 tfrlem7
|-  Fun recs ( F )
4 funex
|-  ( ( Fun recs ( F ) /\ dom recs ( F ) e. On ) -> recs ( F ) e. _V )
5 3 4 mpan
|-  ( dom recs ( F ) e. On -> recs ( F ) e. _V )
6 2 5 mto
|-  -. dom recs ( F ) e. On
7 1 tfrlem8
|-  Ord dom recs ( F )
8 ordeleqon
|-  ( Ord dom recs ( F ) <-> ( dom recs ( F ) e. On \/ dom recs ( F ) = On ) )
9 7 8 mpbi
|-  ( dom recs ( F ) e. On \/ dom recs ( F ) = On )
10 6 9 mtpor
|-  dom recs ( F ) = On