Metamath Proof Explorer

Theorem fzfi

Description: A finite interval of integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Mar-2015)

Ref Expression
Assertion fzfi ( 𝑀 ... 𝑁 ) ∈ Fin

Proof

Step Hyp Ref Expression
1 0fin ⊢ ∅ ∈ Fin
2 eleq1 ⊢ ( ( 𝑀 ... 𝑁 ) = ∅ → ( ( 𝑀 ... 𝑁 ) ∈ Fin ↔ ∅ ∈ Fin ) )
3 1 2 mpbiri ⊢ ( ( 𝑀 ... 𝑁 ) = ∅ → ( 𝑀 ... 𝑁 ) ∈ Fin )
4 fzn0 ⊢ ( ( 𝑀 ... 𝑁 ) ≠ ∅ ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 onfin2 ⊢ ω = ( On ∩ Fin )
6 inss2 ⊢ ( On ∩ Fin ) ⊆ Fin
7 5 6 eqsstri ⊢ ω ⊆ Fin
8 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
9 8 hashgf1o ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ0
10 peano2uz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
11 uznn0sub ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 + 1 ) − 𝑀 ) ∈ ℕ0 )
12 10 11 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 + 1 ) − 𝑀 ) ∈ ℕ0 )
13 f1ocnvdm ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ0 ∧ ( ( 𝑁 + 1 ) − 𝑀 ) ∈ ℕ0 ) → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) ∈ ω )
14 9 12 13 sylancr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) ∈ ω )
15 7 14 sselid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) ∈ Fin )
16 8 fzen2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) ≈ ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) )
17 enfii ⊢ ( ( ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) ∈ Fin ∧ ( 𝑀 ... 𝑁 ) ≈ ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) ) → ( 𝑀 ... 𝑁 ) ∈ Fin )
18 15 16 17 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) ∈ Fin )
19 4 18 sylbi ⊢ ( ( 𝑀 ... 𝑁 ) ≠ ∅ → ( 𝑀 ... 𝑁 ) ∈ Fin )
20 3 19 pm2.61ine ⊢ ( 𝑀 ... 𝑁 ) ∈ Fin