Theorem fzofi

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

	Ref	Expression
Assertion	fzofi	|- ( M ..^ N ) e. Fin

Proof

Step	Hyp	Ref	Expression
1		fzoval	|- ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
2	1	adantl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
3		fzfi	|- ( M ... ( N - 1 ) ) e. Fin
4	2 3	eqeltrdi	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M ..^ N ) e. Fin )
5		fzof	|- ..^ : ( ZZ X. ZZ ) --> ~P ZZ
6	5	fdmi	|- dom ..^ = ( ZZ X. ZZ )
7	6	ndmov	|- ( -. ( M e. ZZ /\ N e. ZZ ) -> ( M ..^ N ) = (/) )
8		0fi	|- (/) e. Fin
9	7 8	eqeltrdi	|- ( -. ( M e. ZZ /\ N e. ZZ ) -> ( M ..^ N ) e. Fin )
10	4 9	pm2.61i	|- ( M ..^ N ) e. Fin