Metamath Proof Explorer


Theorem fzofi

Description: Half-open integer sets are finite. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion fzofi M ..^ N Fin

Proof

Step Hyp Ref Expression
1 fzoval N M ..^ N = M N 1
2 1 adantl M N M ..^ N = M N 1
3 fzfi M N 1 Fin
4 2 3 eqeltrdi M N M ..^ N Fin
5 fzof ..^ : × 𝒫
6 5 fdmi dom ..^ = ×
7 6 ndmov ¬ M N M ..^ N =
8 0fin Fin
9 7 8 eqeltrdi ¬ M N M ..^ N Fin
10 4 9 pm2.61i M ..^ N Fin