This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑅 )