Step | Hyp | Ref
| Expression |
1 | | 1st2nd2 6178 |
. . . . . . 7
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩) |
2 | 1 | adantl 277 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩) |
3 | 2 | fveq2d 5521 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘𝑧) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(1st
‘𝑧), (2nd
‘𝑧)⟩)) |
4 | | df-ov 5880 |
. . . . . . 7
⊢
((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘𝑧)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(1st
‘𝑧), (2nd
‘𝑧)⟩) |
5 | | xp1st 6168 |
. . . . . . . . 9
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
6 | 5 | adantl 277 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
7 | | frecuzrdgrclt.t |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ 𝑇) |
8 | 7 | sseld 3156 |
. . . . . . . . 9
⊢ (𝜑 → ((2nd
‘𝑧) ∈ 𝑆 → (2nd
‘𝑧) ∈ 𝑇)) |
9 | | xp2nd 6169 |
. . . . . . . . 9
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (2nd ‘𝑧) ∈ 𝑆) |
10 | 8, 9 | impel 280 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (2nd ‘𝑧) ∈ 𝑇) |
11 | | peano2uz 9585 |
. . . . . . . . . 10
⊢
((1st ‘𝑧) ∈ (ℤ≥‘𝐶) → ((1st
‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
12 | 6, 11 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
13 | | frecuzrdgrclt.f |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
14 | 13 | ralrimivva 2559 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
15 | 14 | adantr 276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
16 | 9 | adantl 277 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (2nd ‘𝑧) ∈ 𝑆) |
17 | | oveq1 5884 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘𝑧) → (𝑥𝐹𝑦) = ((1st ‘𝑧)𝐹𝑦)) |
18 | 17 | eleq1d 2246 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑧) → ((𝑥𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹𝑦) ∈ 𝑆)) |
19 | | oveq2 5885 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (2nd ‘𝑧) → ((1st
‘𝑧)𝐹𝑦) = ((1st ‘𝑧)𝐹(2nd ‘𝑧))) |
20 | 19 | eleq1d 2246 |
. . . . . . . . . . . 12
⊢ (𝑦 = (2nd ‘𝑧) → (((1st
‘𝑧)𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
21 | 18, 20 | rspc2v 2856 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑆) → (∀𝑥 ∈
(ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
22 | 6, 16, 21 | syl2anc 411 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
23 | 15, 22 | mpd 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆) |
24 | | opelxp 4658 |
. . . . . . . . 9
⊢
(⟨((1st ‘𝑧) + 1), ((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩ ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶) ∧ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
25 | 12, 23, 24 | sylanbrc 417 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ⟨((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩ ∈
((ℤ≥‘𝐶) × 𝑆)) |
26 | | oveq1 5884 |
. . . . . . . . . 10
⊢ (𝑥 = (1st ‘𝑧) → (𝑥 + 1) = ((1st ‘𝑧) + 1)) |
27 | 26, 17 | opeq12d 3788 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑧) → ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩ = ⟨((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹𝑦)⟩) |
28 | 19 | opeq2d 3787 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑧) → ⟨((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹𝑦)⟩ = ⟨((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹(2nd ‘𝑧))⟩) |
29 | | eqid 2177 |
. . . . . . . . 9
⊢ (𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩) = (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩) |
30 | 27, 28, 29 | ovmpog 6011 |
. . . . . . . 8
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑇 ∧ ⟨((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩ ∈
((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘𝑧)) = ⟨((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩) |
31 | 6, 10, 25, 30 | syl3anc 1238 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘𝑧)) = ⟨((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩) |
32 | 4, 31 | eqtr3id 2224 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(1st
‘𝑧), (2nd
‘𝑧)⟩) =
⟨((1st ‘𝑧) + 1), ((1st ‘𝑧)𝐹(2nd ‘𝑧))⟩) |
33 | 32, 25 | eqeltrd 2254 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(1st
‘𝑧), (2nd
‘𝑧)⟩) ∈
((ℤ≥‘𝐶) × 𝑆)) |
34 | 3, 33 | eqeltrd 2254 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
35 | 34 | ralrimiva 2550 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
36 | | frecuzrdgrclt.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℤ) |
37 | | uzid 9544 |
. . . . 5
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
(ℤ≥‘𝐶)) |
38 | 36, 37 | syl 14 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (ℤ≥‘𝐶)) |
39 | | frecuzrdgrclt.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
40 | | opelxp 4658 |
. . . 4
⊢
(⟨𝐶, 𝐴⟩ ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (𝐶 ∈ (ℤ≥‘𝐶) ∧ 𝐴 ∈ 𝑆)) |
41 | 38, 39, 40 | sylanbrc 417 |
. . 3
⊢ (𝜑 → ⟨𝐶, 𝐴⟩ ∈
((ℤ≥‘𝐶) × 𝑆)) |
42 | | frecfcl 6408 |
. . 3
⊢
((∀𝑧 ∈
((ℤ≥‘𝐶) × 𝑆)((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆) ∧ ⟨𝐶, 𝐴⟩ ∈
((ℤ≥‘𝐶) × 𝑆)) → frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩):ω⟶((ℤ≥‘𝐶) × 𝑆)) |
43 | 35, 41, 42 | syl2anc 411 |
. 2
⊢ (𝜑 → frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩):ω⟶((ℤ≥‘𝐶) × 𝑆)) |
44 | | frecuzrdgrclt.r |
. . 3
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) |
45 | 44 | feq1i 5360 |
. 2
⊢ (𝑅:ω⟶((ℤ≥‘𝐶) × 𝑆) ↔ frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩):ω⟶((ℤ≥‘𝐶) × 𝑆)) |
46 | 43, 45 | sylibr 134 |
1
⊢ (𝜑 → 𝑅:ω⟶((ℤ≥‘𝐶) × 𝑆)) |