| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . 3
⊢ (𝑛 = 0 → (1...𝑛) = (1...0)) |
| 2 | | fveq2 6906 |
. . 3
⊢ (𝑛 = 0 → (◡𝐺‘𝑛) = (◡𝐺‘0)) |
| 3 | 1, 2 | breq12d 5156 |
. 2
⊢ (𝑛 = 0 → ((1...𝑛) ≈ (◡𝐺‘𝑛) ↔ (1...0) ≈ (◡𝐺‘0))) |
| 4 | | oveq2 7439 |
. . 3
⊢ (𝑛 = 𝑚 → (1...𝑛) = (1...𝑚)) |
| 5 | | fveq2 6906 |
. . 3
⊢ (𝑛 = 𝑚 → (◡𝐺‘𝑛) = (◡𝐺‘𝑚)) |
| 6 | 4, 5 | breq12d 5156 |
. 2
⊢ (𝑛 = 𝑚 → ((1...𝑛) ≈ (◡𝐺‘𝑛) ↔ (1...𝑚) ≈ (◡𝐺‘𝑚))) |
| 7 | | oveq2 7439 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → (1...𝑛) = (1...(𝑚 + 1))) |
| 8 | | fveq2 6906 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → (◡𝐺‘𝑛) = (◡𝐺‘(𝑚 + 1))) |
| 9 | 7, 8 | breq12d 5156 |
. 2
⊢ (𝑛 = (𝑚 + 1) → ((1...𝑛) ≈ (◡𝐺‘𝑛) ↔ (1...(𝑚 + 1)) ≈ (◡𝐺‘(𝑚 + 1)))) |
| 10 | | oveq2 7439 |
. . 3
⊢ (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁)) |
| 11 | | fveq2 6906 |
. . 3
⊢ (𝑛 = 𝑁 → (◡𝐺‘𝑛) = (◡𝐺‘𝑁)) |
| 12 | 10, 11 | breq12d 5156 |
. 2
⊢ (𝑛 = 𝑁 → ((1...𝑛) ≈ (◡𝐺‘𝑛) ↔ (1...𝑁) ≈ (◡𝐺‘𝑁))) |
| 13 | | 0ex 5307 |
. . . 4
⊢ ∅
∈ V |
| 14 | 13 | enref 9025 |
. . 3
⊢ ∅
≈ ∅ |
| 15 | | fz10 13585 |
. . 3
⊢ (1...0) =
∅ |
| 16 | | 0z 12624 |
. . . . . 6
⊢ 0 ∈
ℤ |
| 17 | | fzennn.1 |
. . . . . 6
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) |
| 18 | 16, 17 | om2uzf1oi 13994 |
. . . . 5
⊢ 𝐺:ω–1-1-onto→(ℤ≥‘0) |
| 19 | | peano1 7910 |
. . . . 5
⊢ ∅
∈ ω |
| 20 | 18, 19 | pm3.2i 470 |
. . . 4
⊢ (𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ ∅
∈ ω) |
| 21 | 16, 17 | om2uz0i 13988 |
. . . 4
⊢ (𝐺‘∅) =
0 |
| 22 | | f1ocnvfv 7298 |
. . . 4
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ ∅
∈ ω) → ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅)) |
| 23 | 20, 21, 22 | mp2 9 |
. . 3
⊢ (◡𝐺‘0) = ∅ |
| 24 | 14, 15, 23 | 3brtr4i 5173 |
. 2
⊢ (1...0)
≈ (◡𝐺‘0) |
| 25 | | simpr 484 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → (1...𝑚) ≈ (◡𝐺‘𝑚)) |
| 26 | | ovex 7464 |
. . . . . . 7
⊢ (𝑚 + 1) ∈ V |
| 27 | | fvex 6919 |
. . . . . . 7
⊢ (◡𝐺‘𝑚) ∈ V |
| 28 | | en2sn 9081 |
. . . . . . 7
⊢ (((𝑚 + 1) ∈ V ∧ (◡𝐺‘𝑚) ∈ V) → {(𝑚 + 1)} ≈ {(◡𝐺‘𝑚)}) |
| 29 | 26, 27, 28 | mp2an 692 |
. . . . . 6
⊢ {(𝑚 + 1)} ≈ {(◡𝐺‘𝑚)} |
| 30 | 29 | a1i 11 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → {(𝑚 + 1)} ≈ {(◡𝐺‘𝑚)}) |
| 31 | | fzp1disj 13623 |
. . . . . 6
⊢
((1...𝑚) ∩
{(𝑚 + 1)}) =
∅ |
| 32 | 31 | a1i 11 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → ((1...𝑚) ∩ {(𝑚 + 1)}) = ∅) |
| 33 | | f1ocnvdm 7305 |
. . . . . . . . . 10
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ 𝑚 ∈
(ℤ≥‘0)) → (◡𝐺‘𝑚) ∈ ω) |
| 34 | 18, 33 | mpan 690 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘0) → (◡𝐺‘𝑚) ∈ ω) |
| 35 | | nn0uz 12920 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
| 36 | 34, 35 | eleq2s 2859 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ (◡𝐺‘𝑚) ∈ ω) |
| 37 | | nnord 7895 |
. . . . . . . 8
⊢ ((◡𝐺‘𝑚) ∈ ω → Ord (◡𝐺‘𝑚)) |
| 38 | | ordirr 6402 |
. . . . . . . 8
⊢ (Ord
(◡𝐺‘𝑚) → ¬ (◡𝐺‘𝑚) ∈ (◡𝐺‘𝑚)) |
| 39 | 36, 37, 38 | 3syl 18 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ ¬ (◡𝐺‘𝑚) ∈ (◡𝐺‘𝑚)) |
| 40 | 39 | adantr 480 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → ¬ (◡𝐺‘𝑚) ∈ (◡𝐺‘𝑚)) |
| 41 | | disjsn 4711 |
. . . . . 6
⊢ (((◡𝐺‘𝑚) ∩ {(◡𝐺‘𝑚)}) = ∅ ↔ ¬ (◡𝐺‘𝑚) ∈ (◡𝐺‘𝑚)) |
| 42 | 40, 41 | sylibr 234 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → ((◡𝐺‘𝑚) ∩ {(◡𝐺‘𝑚)}) = ∅) |
| 43 | | unen 9086 |
. . . . 5
⊢
((((1...𝑚) ≈
(◡𝐺‘𝑚) ∧ {(𝑚 + 1)} ≈ {(◡𝐺‘𝑚)}) ∧ (((1...𝑚) ∩ {(𝑚 + 1)}) = ∅ ∧ ((◡𝐺‘𝑚) ∩ {(◡𝐺‘𝑚)}) = ∅)) → ((1...𝑚) ∪ {(𝑚 + 1)}) ≈ ((◡𝐺‘𝑚) ∪ {(◡𝐺‘𝑚)})) |
| 44 | 25, 30, 32, 42, 43 | syl22anc 839 |
. . . 4
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → ((1...𝑚) ∪ {(𝑚 + 1)}) ≈ ((◡𝐺‘𝑚) ∪ {(◡𝐺‘𝑚)})) |
| 45 | | 1z 12647 |
. . . . . 6
⊢ 1 ∈
ℤ |
| 46 | | 1m1e0 12338 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
| 47 | 46 | fveq2i 6909 |
. . . . . . . . 9
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
| 48 | 35, 47 | eqtr4i 2768 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
| 49 | 48 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
↔ 𝑚 ∈
(ℤ≥‘(1 − 1))) |
| 50 | 49 | biimpi 216 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
(ℤ≥‘(1 − 1))) |
| 51 | | fzsuc2 13622 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ 𝑚
∈ (ℤ≥‘(1 − 1))) → (1...(𝑚 + 1)) = ((1...𝑚) ∪ {(𝑚 + 1)})) |
| 52 | 45, 50, 51 | sylancr 587 |
. . . . 5
⊢ (𝑚 ∈ ℕ0
→ (1...(𝑚 + 1)) =
((1...𝑚) ∪ {(𝑚 + 1)})) |
| 53 | 52 | adantr 480 |
. . . 4
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → (1...(𝑚 + 1)) = ((1...𝑚) ∪ {(𝑚 + 1)})) |
| 54 | | peano2 7912 |
. . . . . . . . 9
⊢ ((◡𝐺‘𝑚) ∈ ω → suc (◡𝐺‘𝑚) ∈ ω) |
| 55 | 36, 54 | syl 17 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ suc (◡𝐺‘𝑚) ∈ ω) |
| 56 | 55, 18 | jctil 519 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ (𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ suc
(◡𝐺‘𝑚) ∈ ω)) |
| 57 | 16, 17 | om2uzsuci 13989 |
. . . . . . . . 9
⊢ ((◡𝐺‘𝑚) ∈ ω → (𝐺‘suc (◡𝐺‘𝑚)) = ((𝐺‘(◡𝐺‘𝑚)) + 1)) |
| 58 | 36, 57 | syl 17 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ (𝐺‘suc (◡𝐺‘𝑚)) = ((𝐺‘(◡𝐺‘𝑚)) + 1)) |
| 59 | 35 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
↔ 𝑚 ∈
(ℤ≥‘0)) |
| 60 | 59 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
(ℤ≥‘0)) |
| 61 | | f1ocnvfv2 7297 |
. . . . . . . . . 10
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ 𝑚 ∈
(ℤ≥‘0)) → (𝐺‘(◡𝐺‘𝑚)) = 𝑚) |
| 62 | 18, 60, 61 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ0
→ (𝐺‘(◡𝐺‘𝑚)) = 𝑚) |
| 63 | 62 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ ((𝐺‘(◡𝐺‘𝑚)) + 1) = (𝑚 + 1)) |
| 64 | 58, 63 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ (𝐺‘suc (◡𝐺‘𝑚)) = (𝑚 + 1)) |
| 65 | | f1ocnvfv 7298 |
. . . . . . 7
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘0) ∧ suc
(◡𝐺‘𝑚) ∈ ω) → ((𝐺‘suc (◡𝐺‘𝑚)) = (𝑚 + 1) → (◡𝐺‘(𝑚 + 1)) = suc (◡𝐺‘𝑚))) |
| 66 | 56, 64, 65 | sylc 65 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ (◡𝐺‘(𝑚 + 1)) = suc (◡𝐺‘𝑚)) |
| 67 | 66 | adantr 480 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → (◡𝐺‘(𝑚 + 1)) = suc (◡𝐺‘𝑚)) |
| 68 | | df-suc 6390 |
. . . . 5
⊢ suc
(◡𝐺‘𝑚) = ((◡𝐺‘𝑚) ∪ {(◡𝐺‘𝑚)}) |
| 69 | 67, 68 | eqtrdi 2793 |
. . . 4
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → (◡𝐺‘(𝑚 + 1)) = ((◡𝐺‘𝑚) ∪ {(◡𝐺‘𝑚)})) |
| 70 | 44, 53, 69 | 3brtr4d 5175 |
. . 3
⊢ ((𝑚 ∈ ℕ0
∧ (1...𝑚) ≈
(◡𝐺‘𝑚)) → (1...(𝑚 + 1)) ≈ (◡𝐺‘(𝑚 + 1))) |
| 71 | 70 | ex 412 |
. 2
⊢ (𝑚 ∈ ℕ0
→ ((1...𝑚) ≈
(◡𝐺‘𝑚) → (1...(𝑚 + 1)) ≈ (◡𝐺‘(𝑚 + 1)))) |
| 72 | 3, 6, 9, 12, 24, 71 | nn0ind 12713 |
1
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ≈
(◡𝐺‘𝑁)) |