This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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