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