Step | Hyp | Ref
| Expression |
1 | | frec2uzzd.a |
. 2
⊢ (𝜑 → 𝐴 ∈ ω) |
2 | | simpr 108 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = 𝐴) → 𝑤 = 𝐴) |
3 | 2 | eleq1d 2147 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 = 𝐴) → (𝑤 ∈ ω ↔ 𝐴 ∈ ω)) |
4 | 2 | fveq2d 5202 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = 𝐴) → (𝐺‘𝑤) = (𝐺‘𝐴)) |
5 | 4 | eleq1d 2147 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 = 𝐴) → ((𝐺‘𝑤) ∈ ℤ ↔ (𝐺‘𝐴) ∈ ℤ)) |
6 | 3, 5 | imbi12d 232 |
. . 3
⊢ ((𝜑 ∧ 𝑤 = 𝐴) → ((𝑤 ∈ ω → (𝐺‘𝑤) ∈ ℤ) ↔ (𝐴 ∈ ω → (𝐺‘𝐴) ∈ ℤ))) |
7 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = ∅ → (𝐺‘𝑤) = (𝐺‘∅)) |
8 | 7 | eleq1d 2147 |
. . . . 5
⊢ (𝑤 = ∅ → ((𝐺‘𝑤) ∈ ℤ ↔ (𝐺‘∅) ∈
ℤ)) |
9 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (𝐺‘𝑤) = (𝐺‘𝑦)) |
10 | 9 | eleq1d 2147 |
. . . . 5
⊢ (𝑤 = 𝑦 → ((𝐺‘𝑤) ∈ ℤ ↔ (𝐺‘𝑦) ∈ ℤ)) |
11 | | fveq2 5198 |
. . . . . 6
⊢ (𝑤 = suc 𝑦 → (𝐺‘𝑤) = (𝐺‘suc 𝑦)) |
12 | 11 | eleq1d 2147 |
. . . . 5
⊢ (𝑤 = suc 𝑦 → ((𝐺‘𝑤) ∈ ℤ ↔ (𝐺‘suc 𝑦) ∈ ℤ)) |
13 | | frec2uz.1 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℤ) |
14 | | frec2uz.2 |
. . . . . . 7
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶) |
15 | 13, 14 | frec2uz0d 9401 |
. . . . . 6
⊢ (𝜑 → (𝐺‘∅) = 𝐶) |
16 | 15, 13 | eqeltrd 2155 |
. . . . 5
⊢ (𝜑 → (𝐺‘∅) ∈
ℤ) |
17 | | zex 8360 |
. . . . . . . . . . . . . . 15
⊢ ℤ
∈ V |
18 | 17 | mptex 5408 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ ↦ (𝑥 + 1)) ∈ V |
19 | | vex 2604 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
20 | 18, 19 | fvex 5215 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V |
21 | 20 | ax-gen 1378 |
. . . . . . . . . . . 12
⊢
∀𝑧((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V |
22 | | frecsuc 6014 |
. . . . . . . . . . . 12
⊢
((∀𝑧((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V ∧ 𝐶 ∈ ℤ ∧ 𝑦 ∈ ω) → (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶)‘suc 𝑦) = ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘(frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶)‘𝑦))) |
23 | 21, 22 | mp3an1 1255 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℤ ∧ 𝑦 ∈ ω) →
(frec((𝑥 ∈ ℤ
↦ (𝑥 + 1)), 𝐶)‘suc 𝑦) = ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘(frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶)‘𝑦))) |
24 | 13, 23 | sylan 277 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶)‘suc 𝑦) = ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘(frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶)‘𝑦))) |
25 | 14 | fveq1i 5199 |
. . . . . . . . . 10
⊢ (𝐺‘suc 𝑦) = (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶)‘suc 𝑦) |
26 | 14 | fveq1i 5199 |
. . . . . . . . . . 11
⊢ (𝐺‘𝑦) = (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶)‘𝑦) |
27 | 26 | fveq2i 5201 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘(𝐺‘𝑦)) = ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘(frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶)‘𝑦)) |
28 | 24, 25, 27 | 3eqtr4g 2138 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (𝐺‘suc 𝑦) = ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘(𝐺‘𝑦))) |
29 | | oveq1 5539 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐺‘𝑦) → (𝑧 + 1) = ((𝐺‘𝑦) + 1)) |
30 | | oveq1 5539 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑥 + 1) = (𝑧 + 1)) |
31 | 30 | cbvmptv 3873 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℤ ↦ (𝑥 + 1)) = (𝑧 ∈ ℤ ↦ (𝑧 + 1)) |
32 | | peano2z 8387 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℤ → (𝑧 + 1) ∈
ℤ) |
33 | 29, 31, 32 | fvmpt3 5272 |
. . . . . . . . 9
⊢ ((𝐺‘𝑦) ∈ ℤ → ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘(𝐺‘𝑦)) = ((𝐺‘𝑦) + 1)) |
34 | 28, 33 | sylan9eq 2133 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (𝐺‘𝑦) ∈ ℤ) → (𝐺‘suc 𝑦) = ((𝐺‘𝑦) + 1)) |
35 | | peano2z 8387 |
. . . . . . . . 9
⊢ ((𝐺‘𝑦) ∈ ℤ → ((𝐺‘𝑦) + 1) ∈ ℤ) |
36 | 35 | adantl 271 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (𝐺‘𝑦) ∈ ℤ) → ((𝐺‘𝑦) + 1) ∈ ℤ) |
37 | 34, 36 | eqeltrd 2155 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (𝐺‘𝑦) ∈ ℤ) → (𝐺‘suc 𝑦) ∈ ℤ) |
38 | 37 | ex 113 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((𝐺‘𝑦) ∈ ℤ → (𝐺‘suc 𝑦) ∈ ℤ)) |
39 | 38 | expcom 114 |
. . . . 5
⊢ (𝑦 ∈ ω → (𝜑 → ((𝐺‘𝑦) ∈ ℤ → (𝐺‘suc 𝑦) ∈ ℤ))) |
40 | 8, 10, 12, 16, 39 | finds2 4342 |
. . . 4
⊢ (𝑤 ∈ ω → (𝜑 → (𝐺‘𝑤) ∈ ℤ)) |
41 | 40 | com12 30 |
. . 3
⊢ (𝜑 → (𝑤 ∈ ω → (𝐺‘𝑤) ∈ ℤ)) |
42 | 1, 6, 41 | vtocld 2651 |
. 2
⊢ (𝜑 → (𝐴 ∈ ω → (𝐺‘𝐴) ∈ ℤ)) |
43 | 1, 42 | mpd 13 |
1
⊢ (𝜑 → (𝐺‘𝐴) ∈ ℤ) |