Step | Hyp | Ref
| Expression |
1 | | oveq2 5832 |
. . 3
⊢ (𝑛 = 0 → (1...𝑛) = (1...0)) |
2 | | fveq2 5468 |
. . 3
⊢ (𝑛 = 0 → (◡𝐺‘𝑛) = (◡𝐺‘0)) |
3 | 1, 2 | breq12d 3978 |
. 2
⊢ (𝑛 = 0 → ((1...𝑛) ≈ (◡𝐺‘𝑛) ↔ (1...0) ≈ (◡𝐺‘0))) |
4 | | oveq2 5832 |
. . 3
⊢ (𝑛 = 𝑚 → (1...𝑛) = (1...𝑚)) |
5 | | fveq2 5468 |
. . 3
⊢ (𝑛 = 𝑚 → (◡𝐺‘𝑛) = (◡𝐺‘𝑚)) |
6 | 4, 5 | breq12d 3978 |
. 2
⊢ (𝑛 = 𝑚 → ((1...𝑛) ≈ (◡𝐺‘𝑛) ↔ (1...𝑚) ≈ (◡𝐺‘𝑚))) |
7 | | oveq2 5832 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → (1...𝑛) = (1...(𝑚 + 1))) |
8 | | fveq2 5468 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → (◡𝐺‘𝑛) = (◡𝐺‘(𝑚 + 1))) |
9 | 7, 8 | breq12d 3978 |
. 2
⊢ (𝑛 = (𝑚 + 1) → ((1...𝑛) ≈ (◡𝐺‘𝑛) ↔ (1...(𝑚 + 1)) ≈ (◡𝐺‘(𝑚 + 1)))) |
10 | | oveq2 5832 |
. . 3
⊢ (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁)) |
11 | | fveq2 5468 |
. . 3
⊢ (𝑛 = 𝑁 → (◡𝐺‘𝑛) = (◡𝐺‘𝑁)) |
12 | 10, 11 | breq12d 3978 |
. 2
⊢ (𝑛 = 𝑁 → ((1...𝑛) ≈ (◡𝐺‘𝑛) ↔ (1...𝑁) ≈ (◡𝐺‘𝑁))) |
13 | | 0ex 4091 |
. . . 4
⊢ ∅
∈ V |
14 | 13 | enref 6710 |
. . 3
⊢ ∅
≈ ∅ |
15 | | fz10 9948 |
. . 3
⊢ (1...0) =
∅ |
16 | | 0zd 9179 |
. . . . . . 7
⊢ (⊤
→ 0 ∈ ℤ) |
17 | | frecfzennn.1 |
. . . . . . 7
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) |
18 | 16, 17 | frec2uzf1od 10305 |
. . . . . 6
⊢ (⊤
→ 𝐺:ω–1-1-onto→(ℤ≥‘0)) |
19 | 18 | mptru 1344 |
. . . . 5
⊢ 𝐺:ω–1-1-onto→(ℤ≥‘0) |
20 | | peano1 4553 |
. . . . 5
⊢ ∅
∈ ω |
21 | 19, 20 | pm3.2i 270 |
. . . 4
⊢ (𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ ∅
∈ ω) |
22 | 16, 17 | frec2uz0d 10298 |
. . . . 5
⊢ (⊤
→ (𝐺‘∅) =
0) |
23 | 22 | mptru 1344 |
. . . 4
⊢ (𝐺‘∅) =
0 |
24 | | f1ocnvfv 5729 |
. . . 4
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ ∅
∈ ω) → ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅)) |
25 | 21, 23, 24 | mp2 16 |
. . 3
⊢ (◡𝐺‘0) = ∅ |
26 | 14, 15, 25 | 3brtr4i 3994 |
. 2
⊢ (1...0)
≈ (◡𝐺‘0) |
27 | | simpr 109 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → (1...𝑚) ≈ (◡𝐺‘𝑚)) |
28 | | peano2nn0 9130 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) |
29 | | zex 9176 |
. . . . . . . . . . . . . . 15
⊢ ℤ
∈ V |
30 | 29 | mptex 5693 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ ↦ (𝑥 + 1)) ∈ V |
31 | | vex 2715 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
32 | 30, 31 | fvex 5488 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V |
33 | 32 | ax-gen 1429 |
. . . . . . . . . . . 12
⊢
∀𝑧((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V |
34 | | 0z 9178 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℤ |
35 | | frecfnom 6348 |
. . . . . . . . . . . 12
⊢
((∀𝑧((𝑥 ∈ ℤ ↦ (𝑥 + 1))‘𝑧) ∈ V ∧ 0 ∈ ℤ) →
frec((𝑥 ∈ ℤ
↦ (𝑥 + 1)), 0) Fn
ω) |
36 | 33, 34, 35 | mp2an 423 |
. . . . . . . . . . 11
⊢
frec((𝑥 ∈
ℤ ↦ (𝑥 + 1)),
0) Fn ω |
37 | 17 | fneq1i 5264 |
. . . . . . . . . . 11
⊢ (𝐺 Fn ω ↔ frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) Fn
ω) |
38 | 36, 37 | mpbir 145 |
. . . . . . . . . 10
⊢ 𝐺 Fn ω |
39 | | omex 4552 |
. . . . . . . . . 10
⊢ ω
∈ V |
40 | | fnex 5689 |
. . . . . . . . . 10
⊢ ((𝐺 Fn ω ∧ ω ∈
V) → 𝐺 ∈
V) |
41 | 38, 39, 40 | mp2an 423 |
. . . . . . . . 9
⊢ 𝐺 ∈ V |
42 | 41 | cnvex 5124 |
. . . . . . . 8
⊢ ◡𝐺 ∈ V |
43 | | vex 2715 |
. . . . . . . 8
⊢ 𝑚 ∈ V |
44 | 42, 43 | fvex 5488 |
. . . . . . 7
⊢ (◡𝐺‘𝑚) ∈ V |
45 | | en2sn 6758 |
. . . . . . 7
⊢ (((𝑚 + 1) ∈ ℕ0
∧ (◡𝐺‘𝑚) ∈ V) → {(𝑚 + 1)} ≈ {(◡𝐺‘𝑚)}) |
46 | 28, 44, 45 | sylancl 410 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ {(𝑚 + 1)} ≈
{(◡𝐺‘𝑚)}) |
47 | 46 | adantr 274 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → {(𝑚 + 1)} ≈ {(◡𝐺‘𝑚)}) |
48 | | fzp1disj 9982 |
. . . . . 6
⊢
((1...𝑚) ∩
{(𝑚 + 1)}) =
∅ |
49 | 48 | a1i 9 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → ((1...𝑚) ∩ {(𝑚 + 1)}) = ∅) |
50 | | f1ocnvdm 5731 |
. . . . . . . . . 10
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ 𝑚 ∈
(ℤ≥‘0)) → (◡𝐺‘𝑚) ∈ ω) |
51 | 19, 50 | mpan 421 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘0) → (◡𝐺‘𝑚) ∈ ω) |
52 | | nn0uz 9473 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
53 | 51, 52 | eleq2s 2252 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ (◡𝐺‘𝑚) ∈ ω) |
54 | | nnord 4571 |
. . . . . . . 8
⊢ ((◡𝐺‘𝑚) ∈ ω → Ord (◡𝐺‘𝑚)) |
55 | | ordirr 4501 |
. . . . . . . 8
⊢ (Ord
(◡𝐺‘𝑚) → ¬ (◡𝐺‘𝑚) ∈ (◡𝐺‘𝑚)) |
56 | 53, 54, 55 | 3syl 17 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ ¬ (◡𝐺‘𝑚) ∈ (◡𝐺‘𝑚)) |
57 | 56 | adantr 274 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → ¬ (◡𝐺‘𝑚) ∈ (◡𝐺‘𝑚)) |
58 | | disjsn 3621 |
. . . . . 6
⊢ (((◡𝐺‘𝑚) ∩ {(◡𝐺‘𝑚)}) = ∅ ↔ ¬ (◡𝐺‘𝑚) ∈ (◡𝐺‘𝑚)) |
59 | 57, 58 | sylibr 133 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → ((◡𝐺‘𝑚) ∩ {(◡𝐺‘𝑚)}) = ∅) |
60 | | unen 6761 |
. . . . 5
⊢
((((1...𝑚) ≈
(◡𝐺‘𝑚) ∧ {(𝑚 + 1)} ≈ {(◡𝐺‘𝑚)}) ∧ (((1...𝑚) ∩ {(𝑚 + 1)}) = ∅ ∧ ((◡𝐺‘𝑚) ∩ {(◡𝐺‘𝑚)}) = ∅)) → ((1...𝑚) ∪ {(𝑚 + 1)}) ≈ ((◡𝐺‘𝑚) ∪ {(◡𝐺‘𝑚)})) |
61 | 27, 47, 49, 59, 60 | syl22anc 1221 |
. . . 4
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → ((1...𝑚) ∪ {(𝑚 + 1)}) ≈ ((◡𝐺‘𝑚) ∪ {(◡𝐺‘𝑚)})) |
62 | | 1z 9193 |
. . . . . 6
⊢ 1 ∈
ℤ |
63 | | 1m1e0 8902 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
64 | 63 | fveq2i 5471 |
. . . . . . . . 9
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
65 | 52, 64 | eqtr4i 2181 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
66 | 65 | eleq2i 2224 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
↔ 𝑚 ∈
(ℤ≥‘(1 − 1))) |
67 | 66 | biimpi 119 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
(ℤ≥‘(1 − 1))) |
68 | | fzsuc2 9981 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ 𝑚
∈ (ℤ≥‘(1 − 1))) → (1...(𝑚 + 1)) = ((1...𝑚) ∪ {(𝑚 + 1)})) |
69 | 62, 67, 68 | sylancr 411 |
. . . . 5
⊢ (𝑚 ∈ ℕ0
→ (1...(𝑚 + 1)) =
((1...𝑚) ∪ {(𝑚 + 1)})) |
70 | 69 | adantr 274 |
. . . 4
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → (1...(𝑚 + 1)) = ((1...𝑚) ∪ {(𝑚 + 1)})) |
71 | | peano2 4554 |
. . . . . . . . 9
⊢ ((◡𝐺‘𝑚) ∈ ω → suc (◡𝐺‘𝑚) ∈ ω) |
72 | 53, 71 | syl 14 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ suc (◡𝐺‘𝑚) ∈ ω) |
73 | 72, 19 | jctil 310 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ (𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ suc
(◡𝐺‘𝑚) ∈ ω)) |
74 | | 0zd 9179 |
. . . . . . . . . 10
⊢ ((◡𝐺‘𝑚) ∈ ω → 0 ∈
ℤ) |
75 | | id 19 |
. . . . . . . . . 10
⊢ ((◡𝐺‘𝑚) ∈ ω → (◡𝐺‘𝑚) ∈ ω) |
76 | 74, 17, 75 | frec2uzsucd 10300 |
. . . . . . . . 9
⊢ ((◡𝐺‘𝑚) ∈ ω → (𝐺‘suc (◡𝐺‘𝑚)) = ((𝐺‘(◡𝐺‘𝑚)) + 1)) |
77 | 53, 76 | syl 14 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ (𝐺‘suc (◡𝐺‘𝑚)) = ((𝐺‘(◡𝐺‘𝑚)) + 1)) |
78 | 52 | eleq2i 2224 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
↔ 𝑚 ∈
(ℤ≥‘0)) |
79 | 78 | biimpi 119 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
(ℤ≥‘0)) |
80 | | f1ocnvfv2 5728 |
. . . . . . . . . 10
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ 𝑚 ∈
(ℤ≥‘0)) → (𝐺‘(◡𝐺‘𝑚)) = 𝑚) |
81 | 19, 79, 80 | sylancr 411 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ0
→ (𝐺‘(◡𝐺‘𝑚)) = 𝑚) |
82 | 81 | oveq1d 5839 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ ((𝐺‘(◡𝐺‘𝑚)) + 1) = (𝑚 + 1)) |
83 | 77, 82 | eqtrd 2190 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ (𝐺‘suc (◡𝐺‘𝑚)) = (𝑚 + 1)) |
84 | | f1ocnvfv 5729 |
. . . . . . 7
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ suc
(◡𝐺‘𝑚) ∈ ω) → ((𝐺‘suc (◡𝐺‘𝑚)) = (𝑚 + 1) → (◡𝐺‘(𝑚 + 1)) = suc (◡𝐺‘𝑚))) |
85 | 73, 83, 84 | sylc 62 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ (◡𝐺‘(𝑚 + 1)) = suc (◡𝐺‘𝑚)) |
86 | 85 | adantr 274 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → (◡𝐺‘(𝑚 + 1)) = suc (◡𝐺‘𝑚)) |
87 | | df-suc 4331 |
. . . . 5
⊢ suc
(◡𝐺‘𝑚) = ((◡𝐺‘𝑚) ∪ {(◡𝐺‘𝑚)}) |
88 | 86, 87 | eqtrdi 2206 |
. . . 4
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → (◡𝐺‘(𝑚 + 1)) = ((◡𝐺‘𝑚) ∪ {(◡𝐺‘𝑚)})) |
89 | 61, 70, 88 | 3brtr4d 3996 |
. . 3
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → (1...(𝑚 + 1)) ≈ (◡𝐺‘(𝑚 + 1))) |
90 | 89 | ex 114 |
. 2
⊢ (𝑚 ∈ ℕ0
→ ((1...𝑚) ≈
(◡𝐺‘𝑚) → (1...(𝑚 + 1)) ≈ (◡𝐺‘(𝑚 + 1)))) |
91 | 3, 6, 9, 12, 26, 90 | nn0ind 9278 |
1
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ≈
(◡𝐺‘𝑁)) |