Step | Hyp | Ref
| Expression |
1 | | frecuzrdgg.n |
. 2
⊢ (𝜑 → 𝑁 ∈ ω) |
2 | | fveq2 5494 |
. . . . . 6
⊢ (𝑤 = ∅ → (𝑅‘𝑤) = (𝑅‘∅)) |
3 | 2 | fveq2d 5498 |
. . . . 5
⊢ (𝑤 = ∅ →
(1st ‘(𝑅‘𝑤)) = (1st ‘(𝑅‘∅))) |
4 | | fveq2 5494 |
. . . . 5
⊢ (𝑤 = ∅ → (𝐺‘𝑤) = (𝐺‘∅)) |
5 | 3, 4 | eqeq12d 2185 |
. . . 4
⊢ (𝑤 = ∅ →
((1st ‘(𝑅‘𝑤)) = (𝐺‘𝑤) ↔ (1st ‘(𝑅‘∅)) = (𝐺‘∅))) |
6 | 5 | imbi2d 229 |
. . 3
⊢ (𝑤 = ∅ → ((𝜑 → (1st
‘(𝑅‘𝑤)) = (𝐺‘𝑤)) ↔ (𝜑 → (1st ‘(𝑅‘∅)) = (𝐺‘∅)))) |
7 | | fveq2 5494 |
. . . . . 6
⊢ (𝑤 = 𝑘 → (𝑅‘𝑤) = (𝑅‘𝑘)) |
8 | 7 | fveq2d 5498 |
. . . . 5
⊢ (𝑤 = 𝑘 → (1st ‘(𝑅‘𝑤)) = (1st ‘(𝑅‘𝑘))) |
9 | | fveq2 5494 |
. . . . 5
⊢ (𝑤 = 𝑘 → (𝐺‘𝑤) = (𝐺‘𝑘)) |
10 | 8, 9 | eqeq12d 2185 |
. . . 4
⊢ (𝑤 = 𝑘 → ((1st ‘(𝑅‘𝑤)) = (𝐺‘𝑤) ↔ (1st ‘(𝑅‘𝑘)) = (𝐺‘𝑘))) |
11 | 10 | imbi2d 229 |
. . 3
⊢ (𝑤 = 𝑘 → ((𝜑 → (1st ‘(𝑅‘𝑤)) = (𝐺‘𝑤)) ↔ (𝜑 → (1st ‘(𝑅‘𝑘)) = (𝐺‘𝑘)))) |
12 | | fveq2 5494 |
. . . . . 6
⊢ (𝑤 = suc 𝑘 → (𝑅‘𝑤) = (𝑅‘suc 𝑘)) |
13 | 12 | fveq2d 5498 |
. . . . 5
⊢ (𝑤 = suc 𝑘 → (1st ‘(𝑅‘𝑤)) = (1st ‘(𝑅‘suc 𝑘))) |
14 | | fveq2 5494 |
. . . . 5
⊢ (𝑤 = suc 𝑘 → (𝐺‘𝑤) = (𝐺‘suc 𝑘)) |
15 | 13, 14 | eqeq12d 2185 |
. . . 4
⊢ (𝑤 = suc 𝑘 → ((1st ‘(𝑅‘𝑤)) = (𝐺‘𝑤) ↔ (1st ‘(𝑅‘suc 𝑘)) = (𝐺‘suc 𝑘))) |
16 | 15 | imbi2d 229 |
. . 3
⊢ (𝑤 = suc 𝑘 → ((𝜑 → (1st ‘(𝑅‘𝑤)) = (𝐺‘𝑤)) ↔ (𝜑 → (1st ‘(𝑅‘suc 𝑘)) = (𝐺‘suc 𝑘)))) |
17 | | fveq2 5494 |
. . . . . 6
⊢ (𝑤 = 𝑁 → (𝑅‘𝑤) = (𝑅‘𝑁)) |
18 | 17 | fveq2d 5498 |
. . . . 5
⊢ (𝑤 = 𝑁 → (1st ‘(𝑅‘𝑤)) = (1st ‘(𝑅‘𝑁))) |
19 | | fveq2 5494 |
. . . . 5
⊢ (𝑤 = 𝑁 → (𝐺‘𝑤) = (𝐺‘𝑁)) |
20 | 18, 19 | eqeq12d 2185 |
. . . 4
⊢ (𝑤 = 𝑁 → ((1st ‘(𝑅‘𝑤)) = (𝐺‘𝑤) ↔ (1st ‘(𝑅‘𝑁)) = (𝐺‘𝑁))) |
21 | 20 | imbi2d 229 |
. . 3
⊢ (𝑤 = 𝑁 → ((𝜑 → (1st ‘(𝑅‘𝑤)) = (𝐺‘𝑤)) ↔ (𝜑 → (1st ‘(𝑅‘𝑁)) = (𝐺‘𝑁)))) |
22 | | frecuzrdgrclt.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℤ) |
23 | | frecuzrdgrclt.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
24 | | op1stg 6126 |
. . . . 5
⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∈ 𝑆) → (1st ‘〈𝐶, 𝐴〉) = 𝐶) |
25 | 22, 23, 24 | syl2anc 409 |
. . . 4
⊢ (𝜑 → (1st
‘〈𝐶, 𝐴〉) = 𝐶) |
26 | | frecuzrdgrclt.r |
. . . . . . 7
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) |
27 | 26 | fveq1i 5495 |
. . . . . 6
⊢ (𝑅‘∅) = (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘∅) |
28 | | opexg 4211 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∈ 𝑆) → 〈𝐶, 𝐴〉 ∈ V) |
29 | | frec0g 6373 |
. . . . . . . 8
⊢
(〈𝐶, 𝐴〉 ∈ V →
(frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘∅) = 〈𝐶, 𝐴〉) |
30 | 28, 29 | syl 14 |
. . . . . . 7
⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∈ 𝑆) → (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘∅) = 〈𝐶, 𝐴〉) |
31 | 22, 23, 30 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘∅) = 〈𝐶, 𝐴〉) |
32 | 27, 31 | eqtrid 2215 |
. . . . 5
⊢ (𝜑 → (𝑅‘∅) = 〈𝐶, 𝐴〉) |
33 | 32 | fveq2d 5498 |
. . . 4
⊢ (𝜑 → (1st
‘(𝑅‘∅)) =
(1st ‘〈𝐶, 𝐴〉)) |
34 | | frecuzrdgg.g |
. . . . 5
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶) |
35 | 22, 34 | frec2uz0d 10342 |
. . . 4
⊢ (𝜑 → (𝐺‘∅) = 𝐶) |
36 | 25, 33, 35 | 3eqtr4d 2213 |
. . 3
⊢ (𝜑 → (1st
‘(𝑅‘∅)) =
(𝐺‘∅)) |
37 | 22, 34 | frec2uzf1od 10349 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ω–1-1-onto→(ℤ≥‘𝐶)) |
38 | | f1of 5440 |
. . . . . . . . . . 11
⊢ (𝐺:ω–1-1-onto→(ℤ≥‘𝐶) → 𝐺:ω⟶(ℤ≥‘𝐶)) |
39 | 37, 38 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ω⟶(ℤ≥‘𝐶)) |
40 | 39 | ad2antlr 486 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → 𝐺:ω⟶(ℤ≥‘𝐶)) |
41 | | simpll 524 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → 𝑘 ∈ ω) |
42 | 40, 41 | ffvelrnd 5629 |
. . . . . . . 8
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (𝐺‘𝑘) ∈ (ℤ≥‘𝐶)) |
43 | | peano2uz 9529 |
. . . . . . . 8
⊢ ((𝐺‘𝑘) ∈ (ℤ≥‘𝐶) → ((𝐺‘𝑘) + 1) ∈
(ℤ≥‘𝐶)) |
44 | 42, 43 | syl 14 |
. . . . . . 7
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → ((𝐺‘𝑘) + 1) ∈
(ℤ≥‘𝐶)) |
45 | | oveq2 5858 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → ((𝐺‘𝑘)𝐹𝑦) = ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))) |
46 | 45 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → (((𝐺‘𝑘)𝐹𝑦) ∈ 𝑆 ↔ ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘))) ∈ 𝑆)) |
47 | | oveq1 5857 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑘) → (𝑥𝐹𝑦) = ((𝐺‘𝑘)𝐹𝑦)) |
48 | 47 | eleq1d 2239 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐺‘𝑘) → ((𝑥𝐹𝑦) ∈ 𝑆 ↔ ((𝐺‘𝑘)𝐹𝑦) ∈ 𝑆)) |
49 | 48 | ralbidv 2470 |
. . . . . . . . 9
⊢ (𝑥 = (𝐺‘𝑘) → (∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 ↔ ∀𝑦 ∈ 𝑆 ((𝐺‘𝑘)𝐹𝑦) ∈ 𝑆)) |
50 | | frecuzrdgrclt.f |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
51 | 50 | ralrimivva 2552 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
52 | 51 | ad2antlr 486 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
53 | 49, 52, 42 | rspcdva 2839 |
. . . . . . . 8
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → ∀𝑦 ∈ 𝑆 ((𝐺‘𝑘)𝐹𝑦) ∈ 𝑆) |
54 | | frecuzrdgrclt.t |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ⊆ 𝑇) |
55 | 22, 23, 54, 50, 26 | frecuzrdgrclt 10358 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅:ω⟶((ℤ≥‘𝐶) × 𝑆)) |
56 | 55 | ad2antlr 486 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → 𝑅:ω⟶((ℤ≥‘𝐶) × 𝑆)) |
57 | 56, 41 | ffvelrnd 5629 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (𝑅‘𝑘) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
58 | | xp2nd 6142 |
. . . . . . . . 9
⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝐶) × 𝑆) → (2nd ‘(𝑅‘𝑘)) ∈ 𝑆) |
59 | 57, 58 | syl 14 |
. . . . . . . 8
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (2nd ‘(𝑅‘𝑘)) ∈ 𝑆) |
60 | 46, 53, 59 | rspcdva 2839 |
. . . . . . 7
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘))) ∈ 𝑆) |
61 | | op1stg 6126 |
. . . . . . 7
⊢ ((((𝐺‘𝑘) + 1) ∈
(ℤ≥‘𝐶) ∧ ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘))) ∈ 𝑆) → (1st
‘〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉) = ((𝐺‘𝑘) + 1)) |
62 | 44, 60, 61 | syl2anc 409 |
. . . . . 6
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (1st
‘〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉) = ((𝐺‘𝑘) + 1)) |
63 | | 1st2nd2 6151 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
64 | 63 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
65 | 64 | fveq2d 5498 |
. . . . . . . . . . . . . 14
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉)) |
66 | | df-ov 5853 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
67 | | xp1st 6141 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
68 | 67 | adantl 275 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (1st ‘𝑧) ∈
(ℤ≥‘𝐶)) |
69 | 54 | ad3antlr 490 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → 𝑆 ⊆ 𝑇) |
70 | | xp2nd 6142 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈
((ℤ≥‘𝐶) × 𝑆) → (2nd ‘𝑧) ∈ 𝑆) |
71 | 70 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (2nd ‘𝑧) ∈ 𝑆) |
72 | 69, 71 | sseldd 3148 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → (2nd ‘𝑧) ∈ 𝑇) |
73 | | peano2uz 9529 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑧) ∈ (ℤ≥‘𝐶) → ((1st
‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
74 | 68, 73 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶)) |
75 | | oveq2 5858 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (2nd ‘𝑧) → ((1st
‘𝑧)𝐹𝑦) = ((1st ‘𝑧)𝐹(2nd ‘𝑧))) |
76 | 75 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (2nd ‘𝑧) → (((1st
‘𝑧)𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆)) |
77 | | oveq1 5857 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (1st ‘𝑧) → (𝑥𝐹𝑦) = ((1st ‘𝑧)𝐹𝑦)) |
78 | 77 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (1st ‘𝑧) → ((𝑥𝐹𝑦) ∈ 𝑆 ↔ ((1st ‘𝑧)𝐹𝑦) ∈ 𝑆)) |
79 | 78 | ralbidv 2470 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (1st ‘𝑧) → (∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆 ↔ ∀𝑦 ∈ 𝑆 ((1st ‘𝑧)𝐹𝑦) ∈ 𝑆)) |
80 | 51 | ad3antlr 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ∀𝑥 ∈ (ℤ≥‘𝐶)∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝑆) |
81 | 79, 80, 68 | rspcdva 2839 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ∀𝑦 ∈ 𝑆 ((1st ‘𝑧)𝐹𝑦) ∈ 𝑆) |
82 | 76, 81, 71 | rspcdva 2839 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆) |
83 | | opelxpi 4641 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1st ‘𝑧) + 1) ∈
(ℤ≥‘𝐶) ∧ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) ∈ 𝑆) → 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
84 | 74, 82, 83 | syl2anc 409 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
85 | | oveq1 5857 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (1st ‘𝑧) → (𝑥 + 1) = ((1st ‘𝑧) + 1)) |
86 | 85, 77 | opeq12d 3771 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (1st ‘𝑧) → 〈(𝑥 + 1), (𝑥𝐹𝑦)〉 = 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹𝑦)〉) |
87 | 75 | opeq2d 3770 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (2nd ‘𝑧) → 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹𝑦)〉 = 〈((1st ‘𝑧) + 1), ((1st
‘𝑧)𝐹(2nd ‘𝑧))〉) |
88 | | eqid 2170 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) = (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) |
89 | 86, 87, 88 | ovmpog 5984 |
. . . . . . . . . . . . . . . . 17
⊢
(((1st ‘𝑧) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘𝑧) ∈ 𝑇 ∧ 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉) |
90 | 68, 72, 84, 89 | syl3anc 1233 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((1st ‘𝑧)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘𝑧)) = 〈((1st
‘𝑧) + 1),
((1st ‘𝑧)𝐹(2nd ‘𝑧))〉) |
91 | 66, 90 | eqtr3id 2217 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) =
〈((1st ‘𝑧) + 1), ((1st ‘𝑧)𝐹(2nd ‘𝑧))〉) |
92 | 91, 84 | eqeltrd 2247 |
. . . . . . . . . . . . . 14
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) ∈
((ℤ≥‘𝐶) × 𝑆)) |
93 | 65, 92 | eqeltrd 2247 |
. . . . . . . . . . . . 13
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) ∧ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
94 | 93 | ralrimiva 2543 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → ∀𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆)((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
95 | | uzid 9488 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
(ℤ≥‘𝐶)) |
96 | 22, 95 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ (ℤ≥‘𝐶)) |
97 | | opelxpi 4641 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈
(ℤ≥‘𝐶) ∧ 𝐴 ∈ 𝑆) → 〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
98 | 96, 23, 97 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
99 | 98 | ad2antlr 486 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → 〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
100 | | frecsuc 6383 |
. . . . . . . . . . . 12
⊢
((∀𝑧 ∈
((ℤ≥‘𝐶) × 𝑆)((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ ((ℤ≥‘𝐶) × 𝑆) ∧ 〈𝐶, 𝐴〉 ∈
((ℤ≥‘𝐶) × 𝑆) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑘))) |
101 | 94, 99, 41, 100 | syl3anc 1233 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑘))) |
102 | 26 | fveq1i 5495 |
. . . . . . . . . . 11
⊢ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc 𝑘) |
103 | 26 | fveq1i 5495 |
. . . . . . . . . . . 12
⊢ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑘) |
104 | 103 | fveq2i 5497 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑘)) |
105 | 101, 102,
104 | 3eqtr4g 2228 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑘))) |
106 | | 1st2nd2 6151 |
. . . . . . . . . . . 12
⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝐶) × 𝑆) → (𝑅‘𝑘) = 〈(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))〉) |
107 | 57, 106 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (𝑅‘𝑘) = 〈(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))〉) |
108 | 107 | fveq2d 5498 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉)) |
109 | 105, 108 | eqtrd 2203 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉)) |
110 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (1st ‘(𝑅‘𝑘)) = (𝐺‘𝑘)) |
111 | 110 | opeq1d 3769 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → 〈(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))〉 = 〈(𝐺‘𝑘), (2nd ‘(𝑅‘𝑘))〉) |
112 | 111 | fveq2d 5498 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑘), (2nd ‘(𝑅‘𝑘))〉)) |
113 | 109, 112 | eqtrd 2203 |
. . . . . . . 8
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑘), (2nd ‘(𝑅‘𝑘))〉)) |
114 | | df-ov 5853 |
. . . . . . . . 9
⊢ ((𝐺‘𝑘)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑘), (2nd ‘(𝑅‘𝑘))〉) |
115 | 54 | ad2antlr 486 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → 𝑆 ⊆ 𝑇) |
116 | 115, 59 | sseldd 3148 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (2nd ‘(𝑅‘𝑘)) ∈ 𝑇) |
117 | | opelxpi 4641 |
. . . . . . . . . . 11
⊢ ((((𝐺‘𝑘) + 1) ∈
(ℤ≥‘𝐶) ∧ ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘))) ∈ 𝑆) → 〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
118 | 44, 60, 117 | syl2anc 409 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → 〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
119 | | oveq1 5857 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐺‘𝑘) → (𝑥 + 1) = ((𝐺‘𝑘) + 1)) |
120 | 119, 47 | opeq12d 3771 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑘) → 〈(𝑥 + 1), (𝑥𝐹𝑦)〉 = 〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹𝑦)〉) |
121 | 45 | opeq2d 3770 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → 〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹𝑦)〉 = 〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉) |
122 | 120, 121,
88 | ovmpog 5984 |
. . . . . . . . . 10
⊢ (((𝐺‘𝑘) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘(𝑅‘𝑘)) ∈ 𝑇 ∧ 〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) → ((𝐺‘𝑘)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑘))) = 〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉) |
123 | 42, 116, 118, 122 | syl3anc 1233 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → ((𝐺‘𝑘)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑘))) = 〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉) |
124 | 114, 123 | eqtr3id 2217 |
. . . . . . . 8
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑘), (2nd ‘(𝑅‘𝑘))〉) = 〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉) |
125 | 113, 124 | eqtrd 2203 |
. . . . . . 7
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (𝑅‘suc 𝑘) = 〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉) |
126 | 125 | fveq2d 5498 |
. . . . . 6
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (1st ‘(𝑅‘suc 𝑘)) = (1st ‘〈((𝐺‘𝑘) + 1), ((𝐺‘𝑘)𝐹(2nd ‘(𝑅‘𝑘)))〉)) |
127 | 22 | ad2antlr 486 |
. . . . . . 7
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → 𝐶 ∈ ℤ) |
128 | 127, 34, 41 | frec2uzsucd 10344 |
. . . . . 6
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (𝐺‘suc 𝑘) = ((𝐺‘𝑘) + 1)) |
129 | 62, 126, 128 | 3eqtr4d 2213 |
. . . . 5
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (1st ‘(𝑅‘suc 𝑘)) = (𝐺‘suc 𝑘)) |
130 | 129 | exp31 362 |
. . . 4
⊢ (𝑘 ∈ ω → (𝜑 → ((1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘) → (1st ‘(𝑅‘suc 𝑘)) = (𝐺‘suc 𝑘)))) |
131 | 130 | a2d 26 |
. . 3
⊢ (𝑘 ∈ ω → ((𝜑 → (1st
‘(𝑅‘𝑘)) = (𝐺‘𝑘)) → (𝜑 → (1st ‘(𝑅‘suc 𝑘)) = (𝐺‘suc 𝑘)))) |
132 | 6, 11, 16, 21, 36, 131 | finds 4582 |
. 2
⊢ (𝑁 ∈ ω → (𝜑 → (1st
‘(𝑅‘𝑁)) = (𝐺‘𝑁))) |
133 | 1, 132 | mpcom 36 |
1
⊢ (𝜑 → (1st
‘(𝑅‘𝑁)) = (𝐺‘𝑁)) |