uzrdg0i

Description: Initial value of a recursive definition generator on upper integers. See comment in om2uzrdg . (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⟩) ↾}_{ω}$
	uzrdg.3	$⊢ S = ran R$
Assertion	uzrdg0i	$⊢ S (C) = A$

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	1 2 3 4 5	uzrdgfni	$⊢ S Fn ℤ_{\geq C}$
7		fnfun	$⊢ S Fn ℤ_{\geq C} \to Fun S$
8	6 7	ax-mp	$⊢ Fun S$
9	4	fveq1i	$⊢ R (\emptyset) = ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset)$
10		opex	$⊢ ⟨C, A⟩ \in V$
11		fr0g	$⊢ ⟨C, A⟩ \in V \to ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset) = ⟨C, A⟩$
12	10 11	ax-mp	$⊢ ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset) = ⟨C, A⟩$
13	9 12	eqtri	$⊢ R (\emptyset) = ⟨C, A⟩$
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		peano1	$⊢ \emptyset \in ω$
18		fnfvelrn	$⊢ (R Fn ω \land \emptyset \in ω) \to R (\emptyset) \in ran R$
19	16 17 18	mp2an	$⊢ R (\emptyset) \in ran R$
20	13 19	eqeltrri	$⊢ ⟨C, A⟩ \in ran R$
21	20 5	eleqtrri	$⊢ ⟨C, A⟩ \in S$
22		funopfv	$⊢ Fun S \to (⟨C, A⟩ \in S \to S (C) = A)$
23	8 21 22	mp2	$⊢ S (C) = A$

Metamath Proof Explorer

Theorem uzrdg0i

Proof