Theorem 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	⊢ 𝐶 ∈ ℤ
	om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
	uzrdg.1	⊢ 𝐴 ∈ V
	uzrdg.2	⊢ 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω )
	uzrdg.3	⊢ 𝑆 = ran 𝑅
Assertion	uzrdg0i	⊢ ( 𝑆 ‘ 𝐶 ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	⊢ 𝐶 ∈ ℤ
2		om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3		uzrdg.1	⊢ 𝐴 ∈ V
4		uzrdg.2	⊢ 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω )
5		uzrdg.3	⊢ 𝑆 = ran 𝑅
6	1 2 3 4 5	uzrdgfni	⊢ 𝑆 Fn ( ℤ≥ ‘ 𝐶 )
7		fnfun	⊢ ( 𝑆 Fn ( ℤ≥ ‘ 𝐶 ) → Fun 𝑆 )
8	6 7	ax-mp	⊢ Fun 𝑆
9	4	fveq1i	⊢ ( 𝑅 ‘ ∅ ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ )
10		opex	⊢ ⟨ 𝐶 , 𝐴 ⟩ ∈ V
11		fr0g	⊢ ( ⟨ 𝐶 , 𝐴 ⟩ ∈ V → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩ )
12	10 11	ax-mp	⊢ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩
13	9 12	eqtri	⊢ ( 𝑅 ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩
14		frfnom	⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω
15	4	fneq1i	⊢ ( 𝑅 Fn ω ↔ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω )
16	14 15	mpbir	⊢ 𝑅 Fn ω
17		peano1	⊢ ∅ ∈ ω
18		fnfvelrn	⊢ ( ( 𝑅 Fn ω ∧ ∅ ∈ ω ) → ( 𝑅 ‘ ∅ ) ∈ ran 𝑅 )
19	16 17 18	mp2an	⊢ ( 𝑅 ‘ ∅ ) ∈ ran 𝑅
20	13 19	eqeltrri	⊢ ⟨ 𝐶 , 𝐴 ⟩ ∈ ran 𝑅
21	20 5	eleqtrri	⊢ ⟨ 𝐶 , 𝐴 ⟩ ∈ 𝑆
22		funopfv	⊢ ( Fun 𝑆 → ( ⟨ 𝐶 , 𝐴 ⟩ ∈ 𝑆 → ( 𝑆 ‘ 𝐶 ) = 𝐴 ) )
23	8 21 22	mp2	⊢ ( 𝑆 ‘ 𝐶 ) = 𝐴