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 𝐶 ∈ ℤ
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 𝑅 )