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 ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω

Proof

Step Hyp Ref Expression
1 rdgfun ⊢ Fun rec ( 𝐹 , 𝐴 )
2 funres ⊢ ( Fun rec ( 𝐹 , 𝐴 ) → Fun ( rec ( 𝐹 , 𝐴 ) ↾ ω ) )
3 1 2 ax-mp ⊢ Fun ( rec ( 𝐹 , 𝐴 ) ↾ ω )
4 dmres ⊢ dom ( rec ( 𝐹 , 𝐴 ) ↾ ω ) = ( ω ∩ dom rec ( 𝐹 , 𝐴 ) )
5 rdgdmlim ⊢ Lim dom rec ( 𝐹 , 𝐴 )
6 limomss ⊢ ( Lim dom rec ( 𝐹 , 𝐴 ) → ω ⊆ dom rec ( 𝐹 , 𝐴 ) )
7 5 6 ax-mp ⊢ ω ⊆ dom rec ( 𝐹 , 𝐴 )
8 dfss2 ⊢ ( ω ⊆ dom rec ( 𝐹 , 𝐴 ) ↔ ( ω ∩ dom rec ( 𝐹 , 𝐴 ) ) = ω )
9 7 8 mpbi ⊢ ( ω ∩ dom rec ( 𝐹 , 𝐴 ) ) = ω
10 4 9 eqtri ⊢ dom ( rec ( 𝐹 , 𝐴 ) ↾ ω ) = ω
11 df-fn ⊢ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω ↔ ( Fun ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ∧ dom ( rec ( 𝐹 , 𝐴 ) ↾ ω ) = ω ) )
12 3 10 11 mpbir2an ⊢ ( rec ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω