Step | Hyp | Ref
| Expression |
1 | | frec2uz.1 |
. 2
⊢ (φ → 𝐶 ∈
ℤ) |
2 | | zex 8030 |
. . . . . . . . . . 11
⊢ ℤ
∈ V |
3 | 2 | mptex 5330 |
. . . . . . . . . 10
⊢ (x ∈ ℤ
↦ (x + 1)) ∈ V |
4 | | vex 2554 |
. . . . . . . . . 10
⊢ z ∈
V |
5 | 3, 4 | fvex 5138 |
. . . . . . . . 9
⊢
((x ∈ ℤ ↦ (x + 1))‘z)
∈ V |
6 | 5 | ax-gen 1335 |
. . . . . . . 8
⊢ ∀z((x ∈ ℤ
↦ (x + 1))‘z) ∈
V |
7 | | frecfnom 5925 |
. . . . . . . 8
⊢ ((∀z((x ∈ ℤ
↦ (x + 1))‘z) ∈ V ∧ 𝐶 ∈
ℤ) → frec((x ∈ ℤ ↦ (x + 1)), 𝐶) Fn 𝜔) |
8 | 6, 7 | mpan 400 |
. . . . . . 7
⊢ (𝐶 ∈ ℤ → frec((x ∈ ℤ
↦ (x + 1)), 𝐶) Fn 𝜔) |
9 | | frec2uz.2 |
. . . . . . . 8
⊢ 𝐺 = frec((x ∈ ℤ
↦ (x + 1)), 𝐶) |
10 | 9 | fneq1i 4936 |
. . . . . . 7
⊢ (𝐺 Fn 𝜔 ↔
frec((x ∈
ℤ ↦ (x + 1)), 𝐶) Fn 𝜔) |
11 | 8, 10 | sylibr 137 |
. . . . . 6
⊢ (𝐶 ∈ ℤ → 𝐺 Fn 𝜔) |
12 | | fvelrnb 5164 |
. . . . . 6
⊢ (𝐺 Fn 𝜔 → (y ∈ ran 𝐺 ↔ ∃z ∈ 𝜔 (𝐺‘z) = y)) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ (𝐶 ∈ ℤ → (y ∈ ran 𝐺 ↔ ∃z ∈ 𝜔 (𝐺‘z) = y)) |
14 | | simpl 102 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℤ ∧
z ∈
𝜔) → 𝐶 ∈ ℤ) |
15 | | simpr 103 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℤ ∧
z ∈
𝜔) → z ∈ 𝜔) |
16 | 14, 9, 15 | frec2uzuzd 8869 |
. . . . . . 7
⊢ ((𝐶 ∈ ℤ ∧
z ∈
𝜔) → (𝐺‘z) ∈
(ℤ≥‘𝐶)) |
17 | | eleq1 2097 |
. . . . . . 7
⊢ ((𝐺‘z) = y →
((𝐺‘z) ∈
(ℤ≥‘𝐶) ↔ y ∈
(ℤ≥‘𝐶))) |
18 | 16, 17 | syl5ibcom 144 |
. . . . . 6
⊢ ((𝐶 ∈ ℤ ∧
z ∈
𝜔) → ((𝐺‘z) = y →
y ∈
(ℤ≥‘𝐶))) |
19 | 18 | rexlimdva 2427 |
. . . . 5
⊢ (𝐶 ∈ ℤ → (∃z ∈ 𝜔 (𝐺‘z) = y →
y ∈
(ℤ≥‘𝐶))) |
20 | 13, 19 | sylbid 139 |
. . . 4
⊢ (𝐶 ∈ ℤ → (y ∈ ran 𝐺 → y ∈
(ℤ≥‘𝐶))) |
21 | | eleq1 2097 |
. . . . 5
⊢ (w = 𝐶 → (w ∈ ran 𝐺 ↔ 𝐶 ∈ ran
𝐺)) |
22 | | eleq1 2097 |
. . . . 5
⊢ (w = y →
(w ∈ ran
𝐺 ↔ y ∈ ran 𝐺)) |
23 | | eleq1 2097 |
. . . . 5
⊢ (w = (y + 1)
→ (w ∈ ran 𝐺 ↔ (y + 1) ∈ ran 𝐺)) |
24 | | id 19 |
. . . . . . 7
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
ℤ) |
25 | 24, 9 | frec2uz0d 8866 |
. . . . . 6
⊢ (𝐶 ∈ ℤ → (𝐺‘∅) = 𝐶) |
26 | | peano1 4260 |
. . . . . . 7
⊢ ∅
∈ 𝜔 |
27 | | fnfvelrn 5242 |
. . . . . . 7
⊢ ((𝐺 Fn 𝜔 ∧ ∅ ∈
𝜔) → (𝐺‘∅) ∈ ran 𝐺) |
28 | 11, 26, 27 | sylancl 392 |
. . . . . 6
⊢ (𝐶 ∈ ℤ → (𝐺‘∅) ∈ ran 𝐺) |
29 | 25, 28 | eqeltrrd 2112 |
. . . . 5
⊢ (𝐶 ∈ ℤ → 𝐶 ∈ ran
𝐺) |
30 | | eluzel2 8254 |
. . . . . 6
⊢ (y ∈
(ℤ≥‘𝐶) → 𝐶 ∈
ℤ) |
31 | 14, 9, 15 | frec2uzsucd 8868 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℤ ∧
z ∈
𝜔) → (𝐺‘suc z) = ((𝐺‘z) + 1)) |
32 | | oveq1 5462 |
. . . . . . . . . . 11
⊢ ((𝐺‘z) = y →
((𝐺‘z) + 1) = (y +
1)) |
33 | 31, 32 | sylan9eq 2089 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ ℤ ∧
z ∈
𝜔) ∧ (𝐺‘z) = y) →
(𝐺‘suc z) = (y +
1)) |
34 | | peano2 4261 |
. . . . . . . . . . . 12
⊢ (z ∈ 𝜔
→ suc z ∈ 𝜔) |
35 | | fnfvelrn 5242 |
. . . . . . . . . . . 12
⊢ ((𝐺 Fn 𝜔 ∧ suc z ∈ 𝜔) → (𝐺‘suc z) ∈ ran 𝐺) |
36 | 11, 34, 35 | syl2an 273 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℤ ∧
z ∈
𝜔) → (𝐺‘suc z) ∈ ran 𝐺) |
37 | 36 | adantr 261 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ ℤ ∧
z ∈
𝜔) ∧ (𝐺‘z) = y) →
(𝐺‘suc z) ∈ ran 𝐺) |
38 | 33, 37 | eqeltrrd 2112 |
. . . . . . . . 9
⊢ (((𝐶 ∈ ℤ ∧
z ∈
𝜔) ∧ (𝐺‘z) = y) →
(y + 1) ∈
ran 𝐺) |
39 | 38 | ex 108 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℤ ∧
z ∈
𝜔) → ((𝐺‘z) = y →
(y + 1) ∈
ran 𝐺)) |
40 | 39 | rexlimdva 2427 |
. . . . . . 7
⊢ (𝐶 ∈ ℤ → (∃z ∈ 𝜔 (𝐺‘z) = y →
(y + 1) ∈
ran 𝐺)) |
41 | 13, 40 | sylbid 139 |
. . . . . 6
⊢ (𝐶 ∈ ℤ → (y ∈ ran 𝐺 → (y + 1) ∈ ran 𝐺)) |
42 | 30, 41 | syl 14 |
. . . . 5
⊢ (y ∈
(ℤ≥‘𝐶) → (y ∈ ran 𝐺 → (y + 1) ∈ ran 𝐺)) |
43 | 21, 22, 23, 22, 29, 42 | uzind4 8307 |
. . . 4
⊢ (y ∈
(ℤ≥‘𝐶) → y ∈ ran 𝐺) |
44 | 20, 43 | impbid1 130 |
. . 3
⊢ (𝐶 ∈ ℤ → (y ∈ ran 𝐺 ↔ y ∈
(ℤ≥‘𝐶))) |
45 | 44 | eqrdv 2035 |
. 2
⊢ (𝐶 ∈ ℤ → ran 𝐺 = (ℤ≥‘𝐶)) |
46 | 1, 45 | syl 14 |
1
⊢ (φ → ran 𝐺 = (ℤ≥‘𝐶)) |