Step | Hyp | Ref
| Expression |
1 | | frec2uz.1 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℤ) |
2 | 1 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 𝐶 ∈ ℤ) |
3 | | frec2uz.2 |
. . . . . 6
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶) |
4 | | uzrdg.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
5 | 4 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 𝑆 ∈ 𝑉) |
6 | | uzrdg.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
7 | 6 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 𝐴 ∈ 𝑆) |
8 | | uzrdg.f |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
9 | 8 | adantlr 460 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
10 | | uzrdg.2 |
. . . . . 6
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) |
11 | | peano2uz 8671 |
. . . . . . 7
⊢ (𝐵 ∈
(ℤ≥‘𝐶) → (𝐵 + 1) ∈
(ℤ≥‘𝐶)) |
12 | 11 | adantl 271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝐵 + 1) ∈
(ℤ≥‘𝐶)) |
13 | 2, 3, 5, 7, 9, 10,
12 | frecuzrdglem 9413 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 〈(𝐵 + 1), (2nd
‘(𝑅‘(◡𝐺‘(𝐵 + 1))))〉 ∈ ran 𝑅) |
14 | | frecuzrdgfn.3 |
. . . . . 6
⊢ (𝜑 → 𝑇 = ran 𝑅) |
15 | 14 | adantr 270 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 𝑇 = ran 𝑅) |
16 | 13, 15 | eleqtrrd 2158 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 〈(𝐵 + 1), (2nd
‘(𝑅‘(◡𝐺‘(𝐵 + 1))))〉 ∈ 𝑇) |
17 | 1, 3, 4, 6, 8, 10,
14 | frecuzrdgfn 9414 |
. . . . . . 7
⊢ (𝜑 → 𝑇 Fn (ℤ≥‘𝐶)) |
18 | | fnfun 5016 |
. . . . . . 7
⊢ (𝑇 Fn
(ℤ≥‘𝐶) → Fun 𝑇) |
19 | 17, 18 | syl 14 |
. . . . . 6
⊢ (𝜑 → Fun 𝑇) |
20 | | funopfv 5234 |
. . . . . 6
⊢ (Fun
𝑇 → (〈(𝐵 + 1), (2nd
‘(𝑅‘(◡𝐺‘(𝐵 + 1))))〉 ∈ 𝑇 → (𝑇‘(𝐵 + 1)) = (2nd ‘(𝑅‘(◡𝐺‘(𝐵 + 1)))))) |
21 | 19, 20 | syl 14 |
. . . . 5
⊢ (𝜑 → (〈(𝐵 + 1), (2nd ‘(𝑅‘(◡𝐺‘(𝐵 + 1))))〉 ∈ 𝑇 → (𝑇‘(𝐵 + 1)) = (2nd ‘(𝑅‘(◡𝐺‘(𝐵 + 1)))))) |
22 | 21 | adantr 270 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (〈(𝐵 + 1), (2nd
‘(𝑅‘(◡𝐺‘(𝐵 + 1))))〉 ∈ 𝑇 → (𝑇‘(𝐵 + 1)) = (2nd ‘(𝑅‘(◡𝐺‘(𝐵 + 1)))))) |
23 | 16, 22 | mpd 13 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝑇‘(𝐵 + 1)) = (2nd ‘(𝑅‘(◡𝐺‘(𝐵 + 1))))) |
24 | 1, 3 | frec2uzf1od 9408 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:ω–1-1-onto→(ℤ≥‘𝐶)) |
25 | | f1ocnvdm 5441 |
. . . . . . . . 9
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘𝐶) ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (◡𝐺‘𝐵) ∈ ω) |
26 | 24, 25 | sylan 277 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (◡𝐺‘𝐵) ∈ ω) |
27 | 2, 3, 26 | frec2uzsucd 9403 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝐺‘suc (◡𝐺‘𝐵)) = ((𝐺‘(◡𝐺‘𝐵)) + 1)) |
28 | | f1ocnvfv2 5438 |
. . . . . . . . 9
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘𝐶) ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝐺‘(◡𝐺‘𝐵)) = 𝐵) |
29 | 24, 28 | sylan 277 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝐺‘(◡𝐺‘𝐵)) = 𝐵) |
30 | 29 | oveq1d 5547 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → ((𝐺‘(◡𝐺‘𝐵)) + 1) = (𝐵 + 1)) |
31 | 27, 30 | eqtrd 2113 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝐺‘suc (◡𝐺‘𝐵)) = (𝐵 + 1)) |
32 | | peano2 4336 |
. . . . . . . 8
⊢ ((◡𝐺‘𝐵) ∈ ω → suc (◡𝐺‘𝐵) ∈ ω) |
33 | 26, 32 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → suc (◡𝐺‘𝐵) ∈ ω) |
34 | | f1ocnvfv 5439 |
. . . . . . . 8
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘𝐶) ∧ suc (◡𝐺‘𝐵) ∈ ω) → ((𝐺‘suc (◡𝐺‘𝐵)) = (𝐵 + 1) → (◡𝐺‘(𝐵 + 1)) = suc (◡𝐺‘𝐵))) |
35 | 24, 34 | sylan 277 |
. . . . . . 7
⊢ ((𝜑 ∧ suc (◡𝐺‘𝐵) ∈ ω) → ((𝐺‘suc (◡𝐺‘𝐵)) = (𝐵 + 1) → (◡𝐺‘(𝐵 + 1)) = suc (◡𝐺‘𝐵))) |
36 | 33, 35 | syldan 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → ((𝐺‘suc (◡𝐺‘𝐵)) = (𝐵 + 1) → (◡𝐺‘(𝐵 + 1)) = suc (◡𝐺‘𝐵))) |
37 | 31, 36 | mpd 13 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (◡𝐺‘(𝐵 + 1)) = suc (◡𝐺‘𝐵)) |
38 | 37 | fveq2d 5202 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝑅‘(◡𝐺‘(𝐵 + 1))) = (𝑅‘suc (◡𝐺‘𝐵))) |
39 | 38 | fveq2d 5202 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (2nd
‘(𝑅‘(◡𝐺‘(𝐵 + 1)))) = (2nd ‘(𝑅‘suc (◡𝐺‘𝐵)))) |
40 | 23, 39 | eqtrd 2113 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝑇‘(𝐵 + 1)) = (2nd ‘(𝑅‘suc (◡𝐺‘𝐵)))) |
41 | | zex 8360 |
. . . . . . . . . . 11
⊢ ℤ
∈ V |
42 | | uzssz 8638 |
. . . . . . . . . . 11
⊢
(ℤ≥‘𝐶) ⊆ ℤ |
43 | 41, 42 | ssexi 3916 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝐶) ∈ V |
44 | | mpt2exga 5855 |
. . . . . . . . . 10
⊢
(((ℤ≥‘𝐶) ∈ V ∧ 𝑆 ∈ 𝑉) → (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) ∈ V) |
45 | 43, 44 | mpan 414 |
. . . . . . . . 9
⊢ (𝑆 ∈ 𝑉 → (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) ∈ V) |
46 | | vex 2604 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
47 | | fvexg 5214 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V) |
48 | 46, 47 | mpan2 415 |
. . . . . . . . 9
⊢ ((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) ∈ V → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V) |
49 | 5, 45, 48 | 3syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V) |
50 | 49 | alrimiv 1795 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → ∀𝑧((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V) |
51 | | opelxp 4392 |
. . . . . . . . 9
⊢
(〈𝐶, 𝐴〉 ∈ (ℤ ×
𝑆) ↔ (𝐶 ∈ ℤ ∧ 𝐴 ∈ 𝑆)) |
52 | 1, 6, 51 | sylanbrc 408 |
. . . . . . . 8
⊢ (𝜑 → 〈𝐶, 𝐴〉 ∈ (ℤ × 𝑆)) |
53 | 52 | adantr 270 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 〈𝐶, 𝐴〉 ∈ (ℤ × 𝑆)) |
54 | | frecsuc 6014 |
. . . . . . 7
⊢
((∀𝑧((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V ∧ 〈𝐶, 𝐴〉 ∈ (ℤ × 𝑆) ∧ (◡𝐺‘𝐵) ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc (◡𝐺‘𝐵)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘(◡𝐺‘𝐵)))) |
55 | 50, 53, 26, 54 | syl3anc 1169 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc (◡𝐺‘𝐵)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘(◡𝐺‘𝐵)))) |
56 | 10 | fveq1i 5199 |
. . . . . 6
⊢ (𝑅‘suc (◡𝐺‘𝐵)) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc (◡𝐺‘𝐵)) |
57 | 10 | fveq1i 5199 |
. . . . . . 7
⊢ (𝑅‘(◡𝐺‘𝐵)) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘(◡𝐺‘𝐵)) |
58 | 57 | fveq2i 5201 |
. . . . . 6
⊢ ((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘(◡𝐺‘𝐵))) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘(◡𝐺‘𝐵))) |
59 | 55, 56, 58 | 3eqtr4g 2138 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝑅‘suc (◡𝐺‘𝐵)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘(◡𝐺‘𝐵)))) |
60 | 2, 3, 5, 7, 9, 10,
26 | frec2uzrdg 9411 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝑅‘(◡𝐺‘𝐵)) = 〈(𝐺‘(◡𝐺‘𝐵)), (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉) |
61 | 60 | fveq2d 5202 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘(◡𝐺‘𝐵))) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘(◡𝐺‘𝐵)), (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉)) |
62 | | df-ov 5535 |
. . . . . 6
⊢ ((𝐺‘(◡𝐺‘𝐵))(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘(◡𝐺‘𝐵)), (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉) |
63 | 61, 62 | syl6eqr 2131 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘(◡𝐺‘𝐵))) = ((𝐺‘(◡𝐺‘𝐵))(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘(◡𝐺‘𝐵))))) |
64 | 2, 3, 26 | frec2uzuzd 9404 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝐺‘(◡𝐺‘𝐵)) ∈
(ℤ≥‘𝐶)) |
65 | 2, 3, 5, 7, 9, 10 | frecuzrdgrrn 9410 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) ∧ (◡𝐺‘𝐵) ∈ ω) → (𝑅‘(◡𝐺‘𝐵)) ∈
((ℤ≥‘𝐶) × 𝑆)) |
66 | 26, 65 | mpdan 412 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝑅‘(◡𝐺‘𝐵)) ∈
((ℤ≥‘𝐶) × 𝑆)) |
67 | | xp2nd 5813 |
. . . . . . 7
⊢ ((𝑅‘(◡𝐺‘𝐵)) ∈
((ℤ≥‘𝐶) × 𝑆) → (2nd ‘(𝑅‘(◡𝐺‘𝐵))) ∈ 𝑆) |
68 | 66, 67 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (2nd
‘(𝑅‘(◡𝐺‘𝐵))) ∈ 𝑆) |
69 | 30, 12 | eqeltrd 2155 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → ((𝐺‘(◡𝐺‘𝐵)) + 1) ∈
(ℤ≥‘𝐶)) |
70 | 9 | caovclg 5673 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) ∧ (𝑧 ∈ (ℤ≥‘𝐶) ∧ 𝑤 ∈ 𝑆)) → (𝑧𝐹𝑤) ∈ 𝑆) |
71 | 70, 64, 68 | caovcld 5674 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) ∈ 𝑆) |
72 | | opexg 3983 |
. . . . . . 7
⊢ ((((𝐺‘(◡𝐺‘𝐵)) + 1) ∈
(ℤ≥‘𝐶) ∧ ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) ∈ 𝑆) → 〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉 ∈ V) |
73 | 69, 71, 72 | syl2anc 403 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉 ∈ V) |
74 | | oveq1 5539 |
. . . . . . . 8
⊢ (𝑧 = (𝐺‘(◡𝐺‘𝐵)) → (𝑧 + 1) = ((𝐺‘(◡𝐺‘𝐵)) + 1)) |
75 | | oveq1 5539 |
. . . . . . . 8
⊢ (𝑧 = (𝐺‘(◡𝐺‘𝐵)) → (𝑧𝐹𝑤) = ((𝐺‘(◡𝐺‘𝐵))𝐹𝑤)) |
76 | 74, 75 | opeq12d 3578 |
. . . . . . 7
⊢ (𝑧 = (𝐺‘(◡𝐺‘𝐵)) → 〈(𝑧 + 1), (𝑧𝐹𝑤)〉 = 〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹𝑤)〉) |
77 | | oveq2 5540 |
. . . . . . . 8
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝐵))) → ((𝐺‘(◡𝐺‘𝐵))𝐹𝑤) = ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))) |
78 | 77 | opeq2d 3577 |
. . . . . . 7
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝐵))) → 〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹𝑤)〉 = 〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉) |
79 | | oveq1 5539 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 + 1) = (𝑧 + 1)) |
80 | | oveq1 5539 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥𝐹𝑦) = (𝑧𝐹𝑦)) |
81 | 79, 80 | opeq12d 3578 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → 〈(𝑥 + 1), (𝑥𝐹𝑦)〉 = 〈(𝑧 + 1), (𝑧𝐹𝑦)〉) |
82 | | oveq2 5540 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → (𝑧𝐹𝑦) = (𝑧𝐹𝑤)) |
83 | 82 | opeq2d 3577 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → 〈(𝑧 + 1), (𝑧𝐹𝑦)〉 = 〈(𝑧 + 1), (𝑧𝐹𝑤)〉) |
84 | 81, 83 | cbvmpt2v 5604 |
. . . . . . 7
⊢ (𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) = (𝑧 ∈ (ℤ≥‘𝐶), 𝑤 ∈ 𝑆 ↦ 〈(𝑧 + 1), (𝑧𝐹𝑤)〉) |
85 | 76, 78, 84 | ovmpt2g 5655 |
. . . . . 6
⊢ (((𝐺‘(◡𝐺‘𝐵)) ∈
(ℤ≥‘𝐶) ∧ (2nd ‘(𝑅‘(◡𝐺‘𝐵))) ∈ 𝑆 ∧ 〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉 ∈ V) → ((𝐺‘(◡𝐺‘𝐵))(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) = 〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉) |
86 | 64, 68, 73, 85 | syl3anc 1169 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → ((𝐺‘(◡𝐺‘𝐵))(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) = 〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉) |
87 | 59, 63, 86 | 3eqtrd 2117 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝑅‘suc (◡𝐺‘𝐵)) = 〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉) |
88 | 87 | fveq2d 5202 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (2nd
‘(𝑅‘suc (◡𝐺‘𝐵))) = (2nd ‘〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉)) |
89 | | op2ndg 5798 |
. . . 4
⊢ ((((𝐺‘(◡𝐺‘𝐵)) + 1) ∈
(ℤ≥‘𝐶) ∧ ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) ∈ 𝑆) → (2nd
‘〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉) = ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))) |
90 | 69, 71, 89 | syl2anc 403 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (2nd
‘〈((𝐺‘(◡𝐺‘𝐵)) + 1), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉) = ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))) |
91 | 88, 90 | eqtrd 2113 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (2nd
‘(𝑅‘suc (◡𝐺‘𝐵))) = ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))) |
92 | | simpr 108 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 𝐵 ∈ (ℤ≥‘𝐶)) |
93 | 2, 3, 5, 7, 9, 10,
92 | frecuzrdglem 9413 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 〈𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉 ∈ ran 𝑅) |
94 | 93, 15 | eleqtrrd 2158 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → 〈𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉 ∈ 𝑇) |
95 | | funopfv 5234 |
. . . . . . 7
⊢ (Fun
𝑇 → (〈𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉 ∈ 𝑇 → (𝑇‘𝐵) = (2nd ‘(𝑅‘(◡𝐺‘𝐵))))) |
96 | 19, 95 | syl 14 |
. . . . . 6
⊢ (𝜑 → (〈𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉 ∈ 𝑇 → (𝑇‘𝐵) = (2nd ‘(𝑅‘(◡𝐺‘𝐵))))) |
97 | 96 | adantr 270 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (〈𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉 ∈ 𝑇 → (𝑇‘𝐵) = (2nd ‘(𝑅‘(◡𝐺‘𝐵))))) |
98 | 94, 97 | mpd 13 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝑇‘𝐵) = (2nd ‘(𝑅‘(◡𝐺‘𝐵)))) |
99 | 98 | eqcomd 2086 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (2nd
‘(𝑅‘(◡𝐺‘𝐵))) = (𝑇‘𝐵)) |
100 | 29, 99 | oveq12d 5550 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) = (𝐵𝐹(𝑇‘𝐵))) |
101 | 40, 91, 100 | 3eqtrd 2117 |
1
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐶)) → (𝑇‘(𝐵 + 1)) = (𝐵𝐹(𝑇‘𝐵))) |