# Metamath Proof Explorer

## Theorem uzrdglem

Description: A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 18-Nov-2014)

Ref Expression
Hypotheses om2uz.1 ${⊢}{C}\in ℤ$
om2uz.2 ${⊢}{G}={\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),{C}\right)↾}_{\mathrm{\omega }}$
uzrdg.1 ${⊢}{A}\in \mathrm{V}$
uzrdg.2 ${⊢}{R}={\mathrm{rec}\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼⟨{x}+1,{x}{F}{y}⟩\right),⟨{C},{A}⟩\right)↾}_{\mathrm{\omega }}$
Assertion uzrdglem ${⊢}{B}\in {ℤ}_{\ge {C}}\to ⟨{B},{2}^{nd}\left({R}\left({{G}}^{-1}\left({B}\right)\right)\right)⟩\in \mathrm{ran}{R}$

### Proof

Step Hyp Ref Expression
1 om2uz.1 ${⊢}{C}\in ℤ$
2 om2uz.2 ${⊢}{G}={\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),{C}\right)↾}_{\mathrm{\omega }}$
3 uzrdg.1 ${⊢}{A}\in \mathrm{V}$
4 uzrdg.2 ${⊢}{R}={\mathrm{rec}\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼⟨{x}+1,{x}{F}{y}⟩\right),⟨{C},{A}⟩\right)↾}_{\mathrm{\omega }}$
5 1 2 om2uzf1oi ${⊢}{G}:\mathrm{\omega }\underset{1-1 onto}{⟶}{ℤ}_{\ge {C}}$
6 f1ocnvdm ${⊢}\left({G}:\mathrm{\omega }\underset{1-1 onto}{⟶}{ℤ}_{\ge {C}}\wedge {B}\in {ℤ}_{\ge {C}}\right)\to {{G}}^{-1}\left({B}\right)\in \mathrm{\omega }$
7 5 6 mpan ${⊢}{B}\in {ℤ}_{\ge {C}}\to {{G}}^{-1}\left({B}\right)\in \mathrm{\omega }$
8 1 2 3 4 om2uzrdg ${⊢}{{G}}^{-1}\left({B}\right)\in \mathrm{\omega }\to {R}\left({{G}}^{-1}\left({B}\right)\right)=⟨{G}\left({{G}}^{-1}\left({B}\right)\right),{2}^{nd}\left({R}\left({{G}}^{-1}\left({B}\right)\right)\right)⟩$
9 7 8 syl ${⊢}{B}\in {ℤ}_{\ge {C}}\to {R}\left({{G}}^{-1}\left({B}\right)\right)=⟨{G}\left({{G}}^{-1}\left({B}\right)\right),{2}^{nd}\left({R}\left({{G}}^{-1}\left({B}\right)\right)\right)⟩$
10 f1ocnvfv2 ${⊢}\left({G}:\mathrm{\omega }\underset{1-1 onto}{⟶}{ℤ}_{\ge {C}}\wedge {B}\in {ℤ}_{\ge {C}}\right)\to {G}\left({{G}}^{-1}\left({B}\right)\right)={B}$
11 5 10 mpan ${⊢}{B}\in {ℤ}_{\ge {C}}\to {G}\left({{G}}^{-1}\left({B}\right)\right)={B}$
12 11 opeq1d ${⊢}{B}\in {ℤ}_{\ge {C}}\to ⟨{G}\left({{G}}^{-1}\left({B}\right)\right),{2}^{nd}\left({R}\left({{G}}^{-1}\left({B}\right)\right)\right)⟩=⟨{B},{2}^{nd}\left({R}\left({{G}}^{-1}\left({B}\right)\right)\right)⟩$
13 9 12 eqtrd ${⊢}{B}\in {ℤ}_{\ge {C}}\to {R}\left({{G}}^{-1}\left({B}\right)\right)=⟨{B},{2}^{nd}\left({R}\left({{G}}^{-1}\left({B}\right)\right)\right)⟩$
14 frfnom ${⊢}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼⟨{x}+1,{x}{F}{y}⟩\right),⟨{C},{A}⟩\right)↾}_{\mathrm{\omega }}\right)Fn\mathrm{\omega }$
15 4 fneq1i ${⊢}{R}Fn\mathrm{\omega }↔\left({\mathrm{rec}\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼⟨{x}+1,{x}{F}{y}⟩\right),⟨{C},{A}⟩\right)↾}_{\mathrm{\omega }}\right)Fn\mathrm{\omega }$
16 14 15 mpbir ${⊢}{R}Fn\mathrm{\omega }$
17 fnfvelrn ${⊢}\left({R}Fn\mathrm{\omega }\wedge {{G}}^{-1}\left({B}\right)\in \mathrm{\omega }\right)\to {R}\left({{G}}^{-1}\left({B}\right)\right)\in \mathrm{ran}{R}$
18 16 7 17 sylancr ${⊢}{B}\in {ℤ}_{\ge {C}}\to {R}\left({{G}}^{-1}\left({B}\right)\right)\in \mathrm{ran}{R}$
19 13 18 eqeltrrd ${⊢}{B}\in {ℤ}_{\ge {C}}\to ⟨{B},{2}^{nd}\left({R}\left({{G}}^{-1}\left({B}\right)\right)\right)⟩\in \mathrm{ran}{R}$