Step | Hyp | Ref
| Expression |
1 | | frecuzrdgrrn.2 |
. . 3
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) |
2 | 1 | fveq1i 5517 |
. 2
⊢ (𝑅‘𝐷) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩)‘𝐷) |
3 | | frec2uz.1 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℤ) |
4 | | uzid 9542 |
. . . . . 6
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
(ℤ≥‘𝐶)) |
5 | 3, 4 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ (ℤ≥‘𝐶)) |
6 | | frecuzrdgrrn.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
7 | | opelxp 4657 |
. . . . 5
⊢
(⟨𝐶, 𝐴⟩ ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (𝐶 ∈ (ℤ≥‘𝐶) ∧ 𝐴 ∈ 𝑆)) |
8 | 5, 6, 7 | sylanbrc 417 |
. . . 4
⊢ (𝜑 → ⟨𝐶, 𝐴⟩ ∈
((ℤ≥‘𝐶) × 𝑆)) |
9 | 8 | adantr 276 |
. . 3
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → ⟨𝐶, 𝐴⟩ ∈
((ℤ≥‘𝐶) × 𝑆)) |
10 | | 1st2nd2 6176 |
. . . . . . 7
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩) |
11 | | fveq2 5516 |
. . . . . . . 8
⊢ (𝑧 = ⟨(1st
‘𝑧), (2nd
‘𝑧)⟩ →
((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘𝑧) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(1st
‘𝑧), (2nd
‘𝑧)⟩)) |
12 | | df-ov 5878 |
. . . . . . . 8
⊢
((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘𝑧)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(1st
‘𝑧), (2nd
‘𝑧)⟩) |
13 | 11, 12 | eqtr4di 2228 |
. . . . . . 7
⊢ (𝑧 = ⟨(1st
‘𝑧), (2nd
‘𝑧)⟩ →
((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘𝑧) = ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘𝑧))) |
14 | 10, 13 | syl 14 |
. . . . . 6
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘𝑧) = ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘𝑧))) |
15 | 14 | adantl 277 |
. . . . 5
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘𝑧) = ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘𝑧))) |
16 | | xp1st 6166 |
. . . . . . 7
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
17 | 16 | adantl 277 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
18 | | xp2nd 6167 |
. . . . . . 7
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (2nd ‘𝑧) ∈ 𝑆) |
19 | 18 | adantl 277 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (2nd ‘𝑧) ∈ 𝑆) |
20 | | peano2uz 9583 |
. . . . . . . 8
⊢
((1st ‘𝑧) ∈ (ℤ≥‘𝐶) → ((1st
‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
21 | 17, 20 | syl 14 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
22 | | frecuzrdgrrn.f |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
23 | 22 | ralrimivva 2559 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
24 | 23 | ad2antrr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
25 | | oveq1 5882 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘𝑧) → (𝑥𝐹𝑦) = ((1st ‘𝑧)𝐹𝑦)) |
26 | 25 | eleq1d 2246 |
. . . . . . . . . 10
⊢ (𝑥 = (1st ‘𝑧) → ((𝑥𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹𝑦) ∈ 𝑆)) |
27 | | oveq2 5883 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘𝑧) → ((1st
‘𝑧)𝐹𝑦) = ((1st ‘𝑧)𝐹(2nd ‘𝑧))) |
28 | 27 | eleq1d 2246 |
. . . . . . . . . 10
⊢ (𝑦 = (2nd ‘𝑧) → (((1st
‘𝑧)𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
29 | 26, 28 | rspc2v 2855 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑆) → (∀𝑥 ∈
(ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
30 | 17, 19, 29 | syl2anc 411 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
31 | 24, 30 | mpd 13 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆) |
32 | | opelxp 4657 |
. . . . . . 7
⊢
(⟨((1st ‘𝑧) + 1), ((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩ ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶) ∧ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
33 | 21, 31, 32 | sylanbrc 417 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ⟨((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩ ∈
((ℤ≥‘𝐶) × 𝑆)) |
34 | | oveq1 5882 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝑧) → (𝑥 + 1) = ((1st ‘𝑧) + 1)) |
35 | 34, 25 | opeq12d 3787 |
. . . . . . 7
⊢ (𝑥 = (1st ‘𝑧) → ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩ = ⟨((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹𝑦)⟩) |
36 | 27 | opeq2d 3786 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝑧) → ⟨((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹𝑦)⟩ = ⟨((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹(2nd ‘𝑧))⟩) |
37 | | eqid 2177 |
. . . . . . 7
⊢ (𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩) = (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩) |
38 | 35, 36, 37 | ovmpog 6009 |
. . . . . 6
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑆 ∧ ⟨((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩ ∈
((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘𝑧)) = ⟨((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩) |
39 | 17, 19, 33, 38 | syl3anc 1238 |
. . . . 5
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘𝑧)) = ⟨((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩) |
40 | 15, 39 | eqtrd 2210 |
. . . 4
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘𝑧) = ⟨((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹(2nd ‘𝑧))⟩) |
41 | 40, 33 | eqeltrd 2254 |
. . 3
⊢ (((𝜑 ∧ 𝐷 ∈ ω) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
42 | | simpr 110 |
. . 3
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → 𝐷 ∈ ω) |
43 | 9, 41, 42 | freccl 6404 |
. 2
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩)‘𝐷) ∈
((ℤ≥‘𝐶) × 𝑆)) |
44 | 2, 43 | eqeltrid 2264 |
1
⊢ ((𝜑 ∧ 𝐷 ∈ ω) → (𝑅‘𝐷) ∈
((ℤ≥‘𝐶) × 𝑆)) |