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 = {rec ((x \in V ⟼ x + 1), C) ↾}_{ω}$
	uzrdg.1	$⊢ A \in V$
	uzrdg.2	$⊢ R = {rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}$
	uzrdg.3	$⊢ S = ran R$
Assertion	uzrdgfni	$⊢ S Fn ℤ_{\geq C}$

Proof

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

Metamath Proof Explorer

Theorem uzrdgfni

Proof