Proof of Theorem fzfi
| Step | Hyp | Ref
| Expression |
| 1 | | 0fi 9082 |
. . 3
⊢ ∅
∈ Fin |
| 2 | | eleq1 2829 |
. . 3
⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈
Fin)) |
| 3 | 1, 2 | mpbiri 258 |
. 2
⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin) |
| 4 | | fzn0 13578 |
. . 3
⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀)) |
| 5 | | onfin2 9268 |
. . . . . 6
⊢ ω =
(On ∩ Fin) |
| 6 | | inss2 4238 |
. . . . . 6
⊢ (On ∩
Fin) ⊆ Fin |
| 7 | 5, 6 | eqsstri 4030 |
. . . . 5
⊢ ω
⊆ Fin |
| 8 | | eqid 2737 |
. . . . . . 7
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) = (rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) |
| 9 | 8 | hashgf1o 14012 |
. . . . . 6
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω):ω–1-1-onto→ℕ0 |
| 10 | | peano2uz 12943 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
| 11 | | uznn0sub 12917 |
. . . . . . 7
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈
ℕ0) |
| 12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈
ℕ0) |
| 13 | | f1ocnvdm 7305 |
. . . . . 6
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω) |
| 14 | 9, 12, 13 | sylancr 587 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω) |
| 15 | 7, 14 | sselid 3981 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin) |
| 16 | 8 | fzen2 14010 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) |
| 17 | | enfii 9226 |
. . . 4
⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin) |
| 18 | 15, 16, 17 | syl2anc 584 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin) |
| 19 | 4, 18 | sylbi 217 |
. 2
⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin) |
| 20 | 3, 19 | pm2.61ine 3025 |
1
⊢ (𝑀...𝑁) ∈ Fin |