Step | Hyp | Ref
| Expression |
1 | | uzrdg.2 |
. . 3
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) |
2 | 1 | fveq1i 5199 |
. 2
⊢ (𝑅‘𝐷) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝐷) |
3 | | zex 8360 |
. . . . . . . 8
⊢ ℤ
∈ V |
4 | | uzssz 8638 |
. . . . . . . 8
⊢
(ℤ≥‘𝐶) ⊆ ℤ |
5 | 3, 4 | ssexi 3916 |
. . . . . . 7
⊢
(ℤ≥‘𝐶) ∈ V |
6 | 5 | a1i 9 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐷 ∈ ω) →
(ℤ≥‘𝐶) ∈ V) |
7 | | uzrdg.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
8 | 7 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → 𝑆 ∈ 𝑉) |
9 | | mpt2exga 5855 |
. . . . . 6
⊢
(((ℤ≥‘𝐶) ∈ V ∧ 𝑆 ∈ 𝑉) → (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) ∈ V) |
10 | 6, 8, 9 | syl2anc 403 |
. . . . 5
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) ∈ V) |
11 | | vex 2604 |
. . . . . 6
⊢ 𝑧 ∈ V |
12 | 11 | a1i 9 |
. . . . 5
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → 𝑧 ∈ V) |
13 | | fvexg 5214 |
. . . . 5
⊢ (((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V) |
14 | 10, 12, 13 | syl2anc 403 |
. . . 4
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V) |
15 | 14 | alrimiv 1795 |
. . 3
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → ∀𝑧((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V) |
16 | | frec2uz.1 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℤ) |
17 | | uzid 8633 |
. . . . . 6
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
(ℤ≥‘𝐶)) |
18 | 16, 17 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ (ℤ≥‘𝐶)) |
19 | | uzrdg.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
20 | | opelxp 4392 |
. . . . 5
⊢
(〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (𝐶 ∈ (ℤ≥‘𝐶) ∧ 𝐴 ∈ 𝑆)) |
21 | 18, 19, 20 | sylanbrc 408 |
. . . 4
⊢ (𝜑 → 〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
22 | 21 | adantr 270 |
. . 3
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → 〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
23 | | 1st2nd2 5821 |
. . . . . . 7
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
24 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 →
((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉)) |
25 | | df-ov 5535 |
. . . . . . . 8
⊢
((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
26 | 24, 25 | syl6eqr 2131 |
. . . . . . 7
⊢ (𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 →
((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧))) |
27 | 23, 26 | syl 14 |
. . . . . 6
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧))) |
28 | 27 | adantl 271 |
. . . . 5
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧))) |
29 | | xp1st 5812 |
. . . . . . 7
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
30 | 29 | adantl 271 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
31 | | xp2nd 5813 |
. . . . . . 7
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (2nd ‘𝑧) ∈ 𝑆) |
32 | 31 | adantl 271 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (2nd ‘𝑧) ∈ 𝑆) |
33 | | peano2uz 8671 |
. . . . . . . 8
⊢
((1st ‘𝑧) ∈ (ℤ≥‘𝐶) → ((1st
‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
34 | 30, 33 | syl 14 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
35 | | uzrdg.f |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
36 | 35 | ralrimivva 2443 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
37 | 36 | ad2antrr 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
38 | | oveq1 5539 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘𝑧) → (𝑥𝐹𝑦) = ((1st ‘𝑧)𝐹𝑦)) |
39 | 38 | eleq1d 2147 |
. . . . . . . . . 10
⊢ (𝑥 = (1st ‘𝑧) → ((𝑥𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹𝑦) ∈ 𝑆)) |
40 | | oveq2 5540 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘𝑧) → ((1st
‘𝑧)𝐹𝑦) = ((1st ‘𝑧)𝐹(2nd ‘𝑧))) |
41 | 40 | eleq1d 2147 |
. . . . . . . . . 10
⊢ (𝑦 = (2nd ‘𝑧) → (((1st
‘𝑧)𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
42 | 39, 41 | rspc2v 2713 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑆) → (∀𝑥 ∈
(ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
43 | 30, 32, 42 | syl2anc 403 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
44 | 37, 43 | mpd 13 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆) |
45 | | opelxp 4392 |
. . . . . . 7
⊢
(〈((1st ‘𝑧) + 1), ((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶) ∧ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
46 | 34, 44, 45 | sylanbrc 408 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
47 | | oveq1 5539 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝑧) → (𝑥 + 1) = ((1st ‘𝑧) + 1)) |
48 | 47, 38 | opeq12d 3578 |
. . . . . . 7
⊢ (𝑥 = (1st ‘𝑧) → 〈(𝑥 + 1), (𝑥𝐹𝑦)〉 = 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹𝑦)〉) |
49 | 40 | opeq2d 3577 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝑧) → 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹𝑦)〉 = 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹(2nd ‘𝑧))〉) |
50 | | eqid 2081 |
. . . . . . 7
⊢ (𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) = (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) |
51 | 48, 49, 50 | ovmpt2g 5655 |
. . . . . 6
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑆 ∧ 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉) |
52 | 30, 32, 46, 51 | syl3anc 1169 |
. . . . 5
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉) |
53 | 28, 52 | eqtrd 2113 |
. . . 4
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹(2nd ‘𝑧))〉) |
54 | 53, 46 | eqeltrd 2155 |
. . 3
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
55 | | simpr 108 |
. . 3
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → 𝐷 ∈ ω) |
56 | 15, 22, 54, 55 | freccl 6016 |
. 2
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝐷) ∈
((ℤ≥‘𝐶) × 𝑆)) |
57 | 2, 56 | syl5eqel 2165 |
1
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → (𝑅‘𝐷) ∈
((ℤ≥‘𝐶) × 𝑆)) |