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 ↾ ω Fn ω

Proof

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