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

Metamath Proof Explorer

Theorem frfnom

Description: The function generated by finite recursive definition generation is a function on omega. (Contributed by NM, 15-Oct-1996) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion frfnom 
|- ( rec ( F , A ) |` _om ) Fn _om

Proof

Step Hyp Ref Expression
1 rdgfun 
 |-  Fun rec ( F , A )
2 funres 
 |-  ( Fun rec ( F , A ) -> Fun ( rec ( F , A ) |` _om ) )
3 1 2 ax-mp 
 |-  Fun ( rec ( F , A ) |` _om )
4 dmres 
 |-  dom ( rec ( F , A ) |` _om ) = ( _om i^i dom rec ( F , A ) )
5 rdgdmlim 
 |-  Lim dom rec ( F , A )
6 limomss 
 |-  ( Lim dom rec ( F , A ) -> _om C_ dom rec ( F , A ) )
7 5 6 ax-mp 
 |-  _om C_ dom rec ( F , A )
8 dfss2 
 |-  ( _om C_ dom rec ( F , A ) <-> ( _om i^i dom rec ( F , A ) ) = _om )
9 7 8 mpbi 
 |-  ( _om i^i dom rec ( F , A ) ) = _om
10 4 9 eqtri 
 |-  dom ( rec ( F , A ) |` _om ) = _om
11 df-fn 
 |-  ( ( rec ( F , A ) |` _om ) Fn _om <-> ( Fun ( rec ( F , A ) |` _om ) /\ dom ( rec ( F , A ) |` _om ) = _om ) )
12 3 10 11 mpbir2an 
 |-  ( rec ( F , A ) |` _om ) Fn _om