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	⊢ 𝐶 ∈ ℤ
	om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
	uzrdg.1	⊢ 𝐴 ∈ V
	uzrdg.2	⊢ 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω )
Assertion	uzrdglem	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ∈ ran 𝑅 )

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	1 2	om2uzf1oi	⊢ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 )
6		f1ocnvdm	⊢ ( ( 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) ) → ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
7	5 6	mpan	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
8	1 2 3 4	om2uzrdg	⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
9	7 8	syl	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
10		f1ocnvfv2	⊢ ( ( 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = 𝐵 )
11	5 10	mpan	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = 𝐵 )
12	11	opeq1d	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ = ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
13	9 12	eqtrd	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
14		frfnom	⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω
15	4	fneq1i	⊢ ( 𝑅 Fn ω ↔ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω )
16	14 15	mpbir	⊢ 𝑅 Fn ω
17		fnfvelrn	⊢ ( ( 𝑅 Fn ω ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ∈ ran 𝑅 )
18	16 7 17	sylancr	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ∈ ran 𝑅 )
19	13 18	eqeltrrd	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ∈ ran 𝑅 )