# Metamath Proof Explorer

## Theorem uzrdgfni

Description: The recursive definition generator on upper integers is a function. See comment in om2uzrdg . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 4-May-2015)

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 }}$
uzrdg.3 ${⊢}{S}=\mathrm{ran}{R}$
Assertion uzrdgfni ${⊢}{S}Fn{ℤ}_{\ge {C}}$

### 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 uzrdg.3 ${⊢}{S}=\mathrm{ran}{R}$
6 5 eleq2i ${⊢}{z}\in {S}↔{z}\in \mathrm{ran}{R}$
7 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 }$
8 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 }$
9 7 8 mpbir ${⊢}{R}Fn\mathrm{\omega }$
10 fvelrnb ${⊢}{R}Fn\mathrm{\omega }\to \left({z}\in \mathrm{ran}{R}↔\exists {w}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{R}\left({w}\right)={z}\right)$
11 9 10 ax-mp ${⊢}{z}\in \mathrm{ran}{R}↔\exists {w}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{R}\left({w}\right)={z}$
12 6 11 bitri ${⊢}{z}\in {S}↔\exists {w}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{R}\left({w}\right)={z}$
13 1 2 3 4 om2uzrdg ${⊢}{w}\in \mathrm{\omega }\to {R}\left({w}\right)=⟨{G}\left({w}\right),{2}^{nd}\left({R}\left({w}\right)\right)⟩$
14 1 2 om2uzuzi ${⊢}{w}\in \mathrm{\omega }\to {G}\left({w}\right)\in {ℤ}_{\ge {C}}$
15 fvex ${⊢}{2}^{nd}\left({R}\left({w}\right)\right)\in \mathrm{V}$
16 opelxpi ${⊢}\left({G}\left({w}\right)\in {ℤ}_{\ge {C}}\wedge {2}^{nd}\left({R}\left({w}\right)\right)\in \mathrm{V}\right)\to ⟨{G}\left({w}\right),{2}^{nd}\left({R}\left({w}\right)\right)⟩\in \left({ℤ}_{\ge {C}}×\mathrm{V}\right)$
17 14 15 16 sylancl ${⊢}{w}\in \mathrm{\omega }\to ⟨{G}\left({w}\right),{2}^{nd}\left({R}\left({w}\right)\right)⟩\in \left({ℤ}_{\ge {C}}×\mathrm{V}\right)$
18 13 17 eqeltrd ${⊢}{w}\in \mathrm{\omega }\to {R}\left({w}\right)\in \left({ℤ}_{\ge {C}}×\mathrm{V}\right)$
19 eleq1 ${⊢}{R}\left({w}\right)={z}\to \left({R}\left({w}\right)\in \left({ℤ}_{\ge {C}}×\mathrm{V}\right)↔{z}\in \left({ℤ}_{\ge {C}}×\mathrm{V}\right)\right)$
20 18 19 syl5ibcom ${⊢}{w}\in \mathrm{\omega }\to \left({R}\left({w}\right)={z}\to {z}\in \left({ℤ}_{\ge {C}}×\mathrm{V}\right)\right)$
21 20 rexlimiv ${⊢}\exists {w}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{R}\left({w}\right)={z}\to {z}\in \left({ℤ}_{\ge {C}}×\mathrm{V}\right)$
22 12 21 sylbi ${⊢}{z}\in {S}\to {z}\in \left({ℤ}_{\ge {C}}×\mathrm{V}\right)$
23 22 ssriv ${⊢}{S}\subseteq {ℤ}_{\ge {C}}×\mathrm{V}$
24 xpss ${⊢}{ℤ}_{\ge {C}}×\mathrm{V}\subseteq \mathrm{V}×\mathrm{V}$
25 23 24 sstri ${⊢}{S}\subseteq \mathrm{V}×\mathrm{V}$
26 df-rel ${⊢}\mathrm{Rel}{S}↔{S}\subseteq \mathrm{V}×\mathrm{V}$
27 25 26 mpbir ${⊢}\mathrm{Rel}{S}$
28 fvex ${⊢}{2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)\in \mathrm{V}$
29 eqeq2 ${⊢}{w}={2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)\to \left({z}={w}↔{z}={2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)\right)$
30 29 imbi2d ${⊢}{w}={2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)\to \left(\left(⟨{v},{z}⟩\in {S}\to {z}={w}\right)↔\left(⟨{v},{z}⟩\in {S}\to {z}={2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)\right)\right)$
31 30 albidv ${⊢}{w}={2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{v},{z}⟩\in {S}\to {z}={w}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{v},{z}⟩\in {S}\to {z}={2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)\right)\right)$
32 28 31 spcev ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{v},{z}⟩\in {S}\to {z}={2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{v},{z}⟩\in {S}\to {z}={w}\right)$
33 5 eleq2i ${⊢}⟨{v},{z}⟩\in {S}↔⟨{v},{z}⟩\in \mathrm{ran}{R}$
34 fvelrnb ${⊢}{R}Fn\mathrm{\omega }\to \left(⟨{v},{z}⟩\in \mathrm{ran}{R}↔\exists {w}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{R}\left({w}\right)=⟨{v},{z}⟩\right)$
35 9 34 ax-mp ${⊢}⟨{v},{z}⟩\in \mathrm{ran}{R}↔\exists {w}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{R}\left({w}\right)=⟨{v},{z}⟩$
36 33 35 bitri ${⊢}⟨{v},{z}⟩\in {S}↔\exists {w}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{R}\left({w}\right)=⟨{v},{z}⟩$
37 13 eqeq1d ${⊢}{w}\in \mathrm{\omega }\to \left({R}\left({w}\right)=⟨{v},{z}⟩↔⟨{G}\left({w}\right),{2}^{nd}\left({R}\left({w}\right)\right)⟩=⟨{v},{z}⟩\right)$
38 fvex ${⊢}{G}\left({w}\right)\in \mathrm{V}$
39 38 15 opth1 ${⊢}⟨{G}\left({w}\right),{2}^{nd}\left({R}\left({w}\right)\right)⟩=⟨{v},{z}⟩\to {G}\left({w}\right)={v}$
40 37 39 syl6bi ${⊢}{w}\in \mathrm{\omega }\to \left({R}\left({w}\right)=⟨{v},{z}⟩\to {G}\left({w}\right)={v}\right)$
41 1 2 om2uzf1oi ${⊢}{G}:\mathrm{\omega }\underset{1-1 onto}{⟶}{ℤ}_{\ge {C}}$
42 f1ocnvfv ${⊢}\left({G}:\mathrm{\omega }\underset{1-1 onto}{⟶}{ℤ}_{\ge {C}}\wedge {w}\in \mathrm{\omega }\right)\to \left({G}\left({w}\right)={v}\to {{G}}^{-1}\left({v}\right)={w}\right)$
43 41 42 mpan ${⊢}{w}\in \mathrm{\omega }\to \left({G}\left({w}\right)={v}\to {{G}}^{-1}\left({v}\right)={w}\right)$
44 40 43 syld ${⊢}{w}\in \mathrm{\omega }\to \left({R}\left({w}\right)=⟨{v},{z}⟩\to {{G}}^{-1}\left({v}\right)={w}\right)$
45 2fveq3 ${⊢}{{G}}^{-1}\left({v}\right)={w}\to {2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)={2}^{nd}\left({R}\left({w}\right)\right)$
46 44 45 syl6 ${⊢}{w}\in \mathrm{\omega }\to \left({R}\left({w}\right)=⟨{v},{z}⟩\to {2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)={2}^{nd}\left({R}\left({w}\right)\right)\right)$
47 46 imp ${⊢}\left({w}\in \mathrm{\omega }\wedge {R}\left({w}\right)=⟨{v},{z}⟩\right)\to {2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)={2}^{nd}\left({R}\left({w}\right)\right)$
48 vex ${⊢}{v}\in \mathrm{V}$
49 vex ${⊢}{z}\in \mathrm{V}$
50 48 49 op2ndd ${⊢}{R}\left({w}\right)=⟨{v},{z}⟩\to {2}^{nd}\left({R}\left({w}\right)\right)={z}$
51 50 adantl ${⊢}\left({w}\in \mathrm{\omega }\wedge {R}\left({w}\right)=⟨{v},{z}⟩\right)\to {2}^{nd}\left({R}\left({w}\right)\right)={z}$
52 47 51 eqtr2d ${⊢}\left({w}\in \mathrm{\omega }\wedge {R}\left({w}\right)=⟨{v},{z}⟩\right)\to {z}={2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)$
53 52 rexlimiva ${⊢}\exists {w}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{R}\left({w}\right)=⟨{v},{z}⟩\to {z}={2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)$
54 36 53 sylbi ${⊢}⟨{v},{z}⟩\in {S}\to {z}={2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)$
55 32 54 mpg ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{v},{z}⟩\in {S}\to {z}={w}\right)$
56 55 ax-gen ${⊢}\forall {v}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{v},{z}⟩\in {S}\to {z}={w}\right)$
57 dffun5 ${⊢}\mathrm{Fun}{S}↔\left(\mathrm{Rel}{S}\wedge \forall {v}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{v},{z}⟩\in {S}\to {z}={w}\right)\right)$
58 27 56 57 mpbir2an ${⊢}\mathrm{Fun}{S}$
59 dmss ${⊢}{S}\subseteq {ℤ}_{\ge {C}}×\mathrm{V}\to \mathrm{dom}{S}\subseteq \mathrm{dom}\left({ℤ}_{\ge {C}}×\mathrm{V}\right)$
60 23 59 ax-mp ${⊢}\mathrm{dom}{S}\subseteq \mathrm{dom}\left({ℤ}_{\ge {C}}×\mathrm{V}\right)$
61 dmxpss ${⊢}\mathrm{dom}\left({ℤ}_{\ge {C}}×\mathrm{V}\right)\subseteq {ℤ}_{\ge {C}}$
62 60 61 sstri ${⊢}\mathrm{dom}{S}\subseteq {ℤ}_{\ge {C}}$
63 1 2 3 4 uzrdglem ${⊢}{v}\in {ℤ}_{\ge {C}}\to ⟨{v},{2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)⟩\in \mathrm{ran}{R}$
64 63 5 eleqtrrdi ${⊢}{v}\in {ℤ}_{\ge {C}}\to ⟨{v},{2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)⟩\in {S}$
65 48 28 opeldm ${⊢}⟨{v},{2}^{nd}\left({R}\left({{G}}^{-1}\left({v}\right)\right)\right)⟩\in {S}\to {v}\in \mathrm{dom}{S}$
66 64 65 syl ${⊢}{v}\in {ℤ}_{\ge {C}}\to {v}\in \mathrm{dom}{S}$
67 66 ssriv ${⊢}{ℤ}_{\ge {C}}\subseteq \mathrm{dom}{S}$
68 62 67 eqssi ${⊢}\mathrm{dom}{S}={ℤ}_{\ge {C}}$
69 df-fn ${⊢}{S}Fn{ℤ}_{\ge {C}}↔\left(\mathrm{Fun}{S}\wedge \mathrm{dom}{S}={ℤ}_{\ge {C}}\right)$
70 58 68 69 mpbir2an ${⊢}{S}Fn{ℤ}_{\ge {C}}$