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 = {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⟩) ↾}_{ω}$
	Assertion	uzrdglem	$⊢ B \in ℤ_{\geq C} \to ⟨B, 2^{nd} (R (G^{-1} (B)))⟩ \in ran R$

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	1 2	om2uzf1oi	$⊢ G : ω \underset{1-1 onto}{⟶} ℤ_{\geq C}$
6		f1ocnvdm	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq C} \land B \in ℤ_{\geq C}) \to G^{-1} (B) \in ω$
7	5 6	mpan	$⊢ B \in ℤ_{\geq C} \to G^{-1} (B) \in ω$
8	1 2 3 4	om2uzrdg	$⊢ G^{-1} (B) \in ω \to R (G^{-1} (B)) = ⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩$
9	7 8	syl	$⊢ B \in ℤ_{\geq C} \to R (G^{-1} (B)) = ⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩$
10		f1ocnvfv2	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq C} \land B \in ℤ_{\geq C}) \to G (G^{-1} (B)) = B$
11	5 10	mpan	$⊢ B \in ℤ_{\geq C} \to G (G^{-1} (B)) = B$
12	11	opeq1d	$⊢ B \in ℤ_{\geq C} \to ⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩ = ⟨B, 2^{nd} (R (G^{-1} (B)))⟩$
13	9 12	eqtrd	$⊢ B \in ℤ_{\geq C} \to R (G^{-1} (B)) = ⟨B, 2^{nd} (R (G^{-1} (B)))⟩$
14		frfnom	$⊢ ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) Fn ω$
15	4	fneq1i	$⊢ R Fn ω \leftrightarrow ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) Fn ω$
16	14 15	mpbir	$⊢ R Fn ω$
17		fnfvelrn	$⊢ (R Fn ω \land G^{-1} (B) \in ω) \to R (G^{-1} (B)) \in ran R$
18	16 7 17	sylancr	$⊢ B \in ℤ_{\geq C} \to R (G^{-1} (B)) \in ran R$
19	13 18	eqeltrrd	$⊢ B \in ℤ_{\geq C} \to ⟨B, 2^{nd} (R (G^{-1} (B)))⟩ \in ran R$