Step | Hyp | Ref
| Expression |
1 | | frecuzrdgrrn.2 |
. . 3
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) |
2 | 1 | fveq1i 5462 |
. 2
⊢ (𝑅‘𝐷) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝐷) |
3 | | frec2uz.1 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℤ) |
4 | | uzid 9432 |
. . . . . 6
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
(ℤ≥‘𝐶)) |
5 | 3, 4 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ (ℤ≥‘𝐶)) |
6 | | frecuzrdgrrn.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
7 | | opelxp 4609 |
. . . . 5
⊢
(〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (𝐶 ∈ (ℤ≥‘𝐶) ∧ 𝐴 ∈ 𝑆)) |
8 | 5, 6, 7 | sylanbrc 414 |
. . . 4
⊢ (𝜑 → 〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
9 | 8 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → 〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
10 | | 1st2nd2 6113 |
. . . . . . 7
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
11 | | fveq2 5461 |
. . . . . . . 8
⊢ (𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 →
((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉)) |
12 | | df-ov 5817 |
. . . . . . . 8
⊢
((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
13 | 11, 12 | eqtr4di 2205 |
. . . . . . 7
⊢ (𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 →
((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧))) |
14 | 10, 13 | syl 14 |
. . . . . 6
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧))) |
15 | 14 | adantl 275 |
. . . . 5
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧))) |
16 | | xp1st 6103 |
. . . . . . 7
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
17 | 16 | adantl 275 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
18 | | xp2nd 6104 |
. . . . . . 7
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (2nd ‘𝑧) ∈ 𝑆) |
19 | 18 | adantl 275 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (2nd ‘𝑧) ∈ 𝑆) |
20 | | peano2uz 9473 |
. . . . . . . 8
⊢
((1st ‘𝑧) ∈ (ℤ≥‘𝐶) → ((1st
‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
21 | 17, 20 | syl 14 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
22 | | frecuzrdgrrn.f |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
23 | 22 | ralrimivva 2536 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
24 | 23 | ad2antrr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
25 | | oveq1 5821 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘𝑧) → (𝑥𝐹𝑦) = ((1st ‘𝑧)𝐹𝑦)) |
26 | 25 | eleq1d 2223 |
. . . . . . . . . 10
⊢ (𝑥 = (1st ‘𝑧) → ((𝑥𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹𝑦) ∈ 𝑆)) |
27 | | oveq2 5822 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘𝑧) → ((1st
‘𝑧)𝐹𝑦) = ((1st ‘𝑧)𝐹(2nd ‘𝑧))) |
28 | 27 | eleq1d 2223 |
. . . . . . . . . 10
⊢ (𝑦 = (2nd ‘𝑧) → (((1st
‘𝑧)𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
29 | 26, 28 | rspc2v 2826 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑆) → (∀𝑥 ∈
(ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
30 | 17, 19, 29 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
31 | 24, 30 | mpd 13 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆) |
32 | | opelxp 4609 |
. . . . . . 7
⊢
(〈((1st ‘𝑧) + 1), ((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶) ∧ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
33 | 21, 31, 32 | sylanbrc 414 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
34 | | oveq1 5821 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝑧) → (𝑥 + 1) = ((1st ‘𝑧) + 1)) |
35 | 34, 25 | opeq12d 3745 |
. . . . . . 7
⊢ (𝑥 = (1st ‘𝑧) → 〈(𝑥 + 1), (𝑥𝐹𝑦)〉 = 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹𝑦)〉) |
36 | 27 | opeq2d 3744 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝑧) → 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹𝑦)〉 = 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹(2nd ‘𝑧))〉) |
37 | | eqid 2154 |
. . . . . . 7
⊢ (𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) = (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) |
38 | 35, 36, 37 | ovmpog 5945 |
. . . . . 6
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑆 ∧ 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉) |
39 | 17, 19, 33, 38 | syl3anc 1217 |
. . . . 5
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉) |
40 | 15, 39 | eqtrd 2187 |
. . . 4
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹(2nd ‘𝑧))〉) |
41 | 40, 33 | eqeltrd 2231 |
. . 3
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
42 | | simpr 109 |
. . 3
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → 𝐷 ∈ ω) |
43 | 9, 41, 42 | freccl 6340 |
. 2
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝐷) ∈
((ℤ≥‘𝐶) × 𝑆)) |
44 | 2, 43 | eqeltrid 2241 |
1
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → (𝑅‘𝐷) ∈
((ℤ≥‘𝐶) × 𝑆)) |