Step | Hyp | Ref
| Expression |
1 | | frec2uzrdg.b |
. 2
⊢ (𝜑 → 𝐵 ∈ ω) |
2 | | fveq2 5494 |
. . . . 5
⊢ (𝑧 = 𝐵 → (𝑅‘𝑧) = (𝑅‘𝐵)) |
3 | | fveq2 5494 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (𝐺‘𝑧) = (𝐺‘𝐵)) |
4 | 2 | fveq2d 5498 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘𝐵))) |
5 | 3, 4 | opeq12d 3771 |
. . . . 5
⊢ (𝑧 = 𝐵 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉) |
6 | 2, 5 | eqeq12d 2185 |
. . . 4
⊢ (𝑧 = 𝐵 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉)) |
7 | 6 | imbi2d 229 |
. . 3
⊢ (𝑧 = 𝐵 → ((𝜑 → (𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉) ↔ (𝜑 → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉))) |
8 | | fveq2 5494 |
. . . . 5
⊢ (𝑧 = ∅ → (𝑅‘𝑧) = (𝑅‘∅)) |
9 | | fveq2 5494 |
. . . . . 6
⊢ (𝑧 = ∅ → (𝐺‘𝑧) = (𝐺‘∅)) |
10 | 8 | fveq2d 5498 |
. . . . . 6
⊢ (𝑧 = ∅ →
(2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘∅))) |
11 | 9, 10 | opeq12d 3771 |
. . . . 5
⊢ (𝑧 = ∅ → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉) |
12 | 8, 11 | eqeq12d 2185 |
. . . 4
⊢ (𝑧 = ∅ → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘∅) = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉)) |
13 | | fveq2 5494 |
. . . . 5
⊢ (𝑧 = 𝑣 → (𝑅‘𝑧) = (𝑅‘𝑣)) |
14 | | fveq2 5494 |
. . . . . 6
⊢ (𝑧 = 𝑣 → (𝐺‘𝑧) = (𝐺‘𝑣)) |
15 | 13 | fveq2d 5498 |
. . . . . 6
⊢ (𝑧 = 𝑣 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘𝑣))) |
16 | 14, 15 | opeq12d 3771 |
. . . . 5
⊢ (𝑧 = 𝑣 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) |
17 | 13, 16 | eqeq12d 2185 |
. . . 4
⊢ (𝑧 = 𝑣 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) |
18 | | fveq2 5494 |
. . . . 5
⊢ (𝑧 = suc 𝑣 → (𝑅‘𝑧) = (𝑅‘suc 𝑣)) |
19 | | fveq2 5494 |
. . . . . 6
⊢ (𝑧 = suc 𝑣 → (𝐺‘𝑧) = (𝐺‘suc 𝑣)) |
20 | 18 | fveq2d 5498 |
. . . . . 6
⊢ (𝑧 = suc 𝑣 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘suc 𝑣))) |
21 | 19, 20 | opeq12d 3771 |
. . . . 5
⊢ (𝑧 = suc 𝑣 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉) |
22 | 18, 21 | eqeq12d 2185 |
. . . 4
⊢ (𝑧 = suc 𝑣 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉)) |
23 | | frecuzrdgrrn.2 |
. . . . . . 7
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) |
24 | 23 | fveq1i 5495 |
. . . . . 6
⊢ (𝑅‘∅) = (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘∅) |
25 | | frec2uz.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℤ) |
26 | | frecuzrdgrrn.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
27 | | opexg 4211 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∈ 𝑆) → 〈𝐶, 𝐴〉 ∈ V) |
28 | 25, 26, 27 | syl2anc 409 |
. . . . . . 7
⊢ (𝜑 → 〈𝐶, 𝐴〉 ∈ V) |
29 | | frec0g 6373 |
. . . . . . 7
⊢
(〈𝐶, 𝐴〉 ∈ V →
(frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘∅) = 〈𝐶, 𝐴〉) |
30 | 28, 29 | syl 14 |
. . . . . 6
⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘∅) = 〈𝐶, 𝐴〉) |
31 | 24, 30 | eqtrid 2215 |
. . . . 5
⊢ (𝜑 → (𝑅‘∅) = 〈𝐶, 𝐴〉) |
32 | | frec2uz.2 |
. . . . . . 7
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶) |
33 | 25, 32 | frec2uz0d 10342 |
. . . . . 6
⊢ (𝜑 → (𝐺‘∅) = 𝐶) |
34 | 31 | fveq2d 5498 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘(𝑅‘∅)) =
(2nd ‘〈𝐶, 𝐴〉)) |
35 | | uzid 9488 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
(ℤ≥‘𝐶)) |
36 | 25, 35 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (ℤ≥‘𝐶)) |
37 | | op2ndg 6127 |
. . . . . . . 8
⊢ ((𝐶 ∈
(ℤ≥‘𝐶) ∧ 𝐴 ∈ 𝑆) → (2nd ‘〈𝐶, 𝐴〉) = 𝐴) |
38 | 36, 26, 37 | syl2anc 409 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘〈𝐶, 𝐴〉) = 𝐴) |
39 | 34, 38 | eqtrd 2203 |
. . . . . 6
⊢ (𝜑 → (2nd
‘(𝑅‘∅)) =
𝐴) |
40 | 33, 39 | opeq12d 3771 |
. . . . 5
⊢ (𝜑 → 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉 = 〈𝐶, 𝐴〉) |
41 | 31, 40 | eqtr4d 2206 |
. . . 4
⊢ (𝜑 → (𝑅‘∅) = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉) |
42 | | 1st2nd2 6151 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
43 | 42 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
44 | 43 | fveq2d 5498 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉)) |
45 | | df-ov 5853 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
46 | | xp1st 6141 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
47 | 46 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
48 | | xp2nd 6142 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (2nd ‘𝑧) ∈ 𝑆) |
49 | 48 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (2nd ‘𝑧) ∈ 𝑆) |
50 | | peano2uz 9529 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑧) ∈ (ℤ≥‘𝐶) → ((1st
‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
51 | 47, 50 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
52 | | frecuzrdgrrn.f |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
53 | 52 | ralrimivva 2552 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
54 | 53 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
55 | | oveq1 5857 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (1st ‘𝑧) → (𝑥𝐹𝑦) = ((1st ‘𝑧)𝐹𝑦)) |
56 | 55 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (1st ‘𝑧) → ((𝑥𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹𝑦) ∈ 𝑆)) |
57 | | oveq2 5858 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (2nd ‘𝑧) → ((1st
‘𝑧)𝐹𝑦) = ((1st ‘𝑧)𝐹(2nd ‘𝑧))) |
58 | 57 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (2nd ‘𝑧) → (((1st
‘𝑧)𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
59 | 56, 58 | rspc2v 2847 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑆) → (∀𝑥 ∈
(ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
60 | 47, 49, 59 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
61 | 54, 60 | mpd 13 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆) |
62 | | opelxp 4639 |
. . . . . . . . . . . . . . . . 17
⊢
(〈((1st ‘𝑧) + 1), ((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶) ∧ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
63 | 51, 61, 62 | sylanbrc 415 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
64 | | oveq1 5857 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (1st ‘𝑧) → (𝑥 + 1) = ((1st ‘𝑧) + 1)) |
65 | 64, 55 | opeq12d 3771 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (1st ‘𝑧) → 〈(𝑥 + 1), (𝑥𝐹𝑦)〉 = 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹𝑦)〉) |
66 | 57 | opeq2d 3770 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (2nd ‘𝑧) → 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹𝑦)〉 = 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹(2nd ‘𝑧))〉) |
67 | | eqid 2170 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) = (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) |
68 | 65, 66, 67 | ovmpog 5984 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑆 ∧ 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉) |
69 | 47, 49, 63, 68 | syl3anc 1233 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉) |
70 | 45, 69 | eqtr3id 2217 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) =
〈((1st ‘𝑧) + 1), ((1st ‘𝑧)𝐹(2nd ‘𝑧))〉) |
71 | 70, 63 | eqeltrd 2247 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) ∈
((ℤ≥‘𝐶) × 𝑆)) |
72 | 44, 71 | eqeltrd 2247 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
73 | 72 | ralrimiva 2543 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ∀𝑧 ∈
((ℤ≥‘𝐶) × 𝑆)((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
74 | 36 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝐶 ∈ (ℤ≥‘𝐶)) |
75 | 26 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝐴 ∈ 𝑆) |
76 | | opelxp 4639 |
. . . . . . . . . . . 12
⊢
(〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (𝐶 ∈ (ℤ≥‘𝐶) ∧ 𝐴 ∈ 𝑆)) |
77 | 74, 75, 76 | sylanbrc 415 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
78 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝑣 ∈ ω) |
79 | | frecsuc 6383 |
. . . . . . . . . . 11
⊢
((∀𝑧 ∈
((ℤ≥‘𝐶) × 𝑆)((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆) ∧ 〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆) ∧ 𝑣 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc 𝑣) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑣))) |
80 | 73, 77, 78, 79 | syl3anc 1233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc 𝑣) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑣))) |
81 | 23 | fveq1i 5495 |
. . . . . . . . . 10
⊢ (𝑅‘suc 𝑣) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc 𝑣) |
82 | 23 | fveq1i 5495 |
. . . . . . . . . . 11
⊢ (𝑅‘𝑣) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑣) |
83 | 82 | fveq2i 5497 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑣)) |
84 | 80, 81, 83 | 3eqtr4g 2228 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝑅‘suc 𝑣) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣))) |
85 | 84 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝑅‘suc 𝑣) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣))) |
86 | | fveq2 5494 |
. . . . . . . . 9
⊢ ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) |
87 | | df-ov 5853 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑣)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) |
88 | 25 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝐶 ∈ ℤ) |
89 | 88, 32, 78 | frec2uzuzd 10345 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝐺‘𝑣) ∈ (ℤ≥‘𝐶)) |
90 | 25, 32, 26, 52, 23 | frecuzrdgrrn 10351 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝑅‘𝑣) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
91 | | xp2nd 6142 |
. . . . . . . . . . . 12
⊢ ((𝑅‘𝑣) ∈ ((ℤ≥‘𝐶) × 𝑆) → (2nd ‘(𝑅‘𝑣)) ∈ 𝑆) |
92 | 90, 91 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (2nd
‘(𝑅‘𝑣)) ∈ 𝑆) |
93 | | peano2uz 9529 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘𝑣) ∈ (ℤ≥‘𝐶) → ((𝐺‘𝑣) + 1) ∈
(ℤ≥‘𝐶)) |
94 | 89, 93 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝐺‘𝑣) + 1) ∈
(ℤ≥‘𝐶)) |
95 | 52 | caovclg 6002 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (ℤ≥‘𝐶) ∧ 𝑤 ∈ 𝑆)) → (𝑧𝐹𝑤) ∈ 𝑆) |
96 | 95 | adantlr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑧 ∈ (ℤ≥‘𝐶) ∧ 𝑤 ∈ 𝑆)) → (𝑧𝐹𝑤) ∈ 𝑆) |
97 | 96, 89, 92 | caovcld 6003 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ 𝑆) |
98 | | opelxp 4639 |
. . . . . . . . . . . 12
⊢
(〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (((𝐺‘𝑣) + 1) ∈
(ℤ≥‘𝐶) ∧ ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ 𝑆)) |
99 | 94, 97, 98 | sylanbrc 415 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
100 | | oveq1 5857 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐺‘𝑣) → (𝑤 + 1) = ((𝐺‘𝑣) + 1)) |
101 | | oveq1 5857 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐺‘𝑣) → (𝑤𝐹𝑧) = ((𝐺‘𝑣)𝐹𝑧)) |
102 | 100, 101 | opeq12d 3771 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐺‘𝑣) → 〈(𝑤 + 1), (𝑤𝐹𝑧)〉 = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹𝑧)〉) |
103 | | oveq2 5858 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (2nd ‘(𝑅‘𝑣)) → ((𝐺‘𝑣)𝐹𝑧) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
104 | 103 | opeq2d 3770 |
. . . . . . . . . . . 12
⊢ (𝑧 = (2nd ‘(𝑅‘𝑣)) → 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹𝑧)〉 = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
105 | | oveq1 5857 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝑥 + 1) = (𝑤 + 1)) |
106 | | oveq1 5857 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝑥𝐹𝑦) = (𝑤𝐹𝑦)) |
107 | 105, 106 | opeq12d 3771 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → 〈(𝑥 + 1), (𝑥𝐹𝑦)〉 = 〈(𝑤 + 1), (𝑤𝐹𝑦)〉) |
108 | | oveq2 5858 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → (𝑤𝐹𝑦) = (𝑤𝐹𝑧)) |
109 | 108 | opeq2d 3770 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → 〈(𝑤 + 1), (𝑤𝐹𝑦)〉 = 〈(𝑤 + 1), (𝑤𝐹𝑧)〉) |
110 | 107, 109 | cbvmpov 5930 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) = (𝑤 ∈ (ℤ≥‘𝐶), 𝑧 ∈ 𝑆 ↦ 〈(𝑤 + 1), (𝑤𝐹𝑧)〉) |
111 | 102, 104,
110 | ovmpog 5984 |
. . . . . . . . . . 11
⊢ (((𝐺‘𝑣) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘(𝑅‘𝑣)) ∈ 𝑆 ∧ 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) → ((𝐺‘𝑣)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
112 | 89, 92, 99, 111 | syl3anc 1233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝐺‘𝑣)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
113 | 87, 112 | eqtr3id 2217 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
114 | 86, 113 | sylan9eqr 2225 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
115 | 85, 114 | eqtrd 2203 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝑅‘suc 𝑣) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
116 | 88, 32, 78 | frec2uzsucd 10344 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝐺‘suc 𝑣) = ((𝐺‘𝑣) + 1)) |
117 | 116 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝐺‘suc 𝑣) = ((𝐺‘𝑣) + 1)) |
118 | 115 | fveq2d 5498 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (2nd
‘(𝑅‘suc 𝑣)) = (2nd
‘〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉)) |
119 | 88, 32, 78 | frec2uzzd 10343 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝐺‘𝑣) ∈ ℤ) |
120 | 119 | peano2zd 9324 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝐺‘𝑣) + 1) ∈ ℤ) |
121 | 120 | adantr 274 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → ((𝐺‘𝑣) + 1) ∈ ℤ) |
122 | 97 | adantr 274 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ 𝑆) |
123 | | op2ndg 6127 |
. . . . . . . . . 10
⊢ ((((𝐺‘𝑣) + 1) ∈ ℤ ∧ ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ 𝑆) → (2nd
‘〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
124 | 121, 122,
123 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (2nd
‘〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
125 | 118, 124 | eqtrd 2203 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (2nd
‘(𝑅‘suc 𝑣)) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
126 | 117, 125 | opeq12d 3771 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉 = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
127 | 115, 126 | eqtr4d 2206 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉) |
128 | 127 | ex 114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉)) |
129 | 128 | expcom 115 |
. . . 4
⊢ (𝑣 ∈ ω → (𝜑 → ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉))) |
130 | 12, 17, 22, 41, 129 | finds2 4583 |
. . 3
⊢ (𝑧 ∈ ω → (𝜑 → (𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉)) |
131 | 7, 130 | vtoclga 2796 |
. 2
⊢ (𝐵 ∈ ω → (𝜑 → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉)) |
132 | 1, 131 | mpcom 36 |
1
⊢ (𝜑 → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉) |