fzofi

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

		Ref	Expression
	Assertion	fzofi	$⊢ (M ..^N) \in Fin$

Step	Hyp	Ref	Expression
1		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
2	1	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to (M ..^N) = (M \dots N - 1)$
3		fzfi	$⊢ (M \dots N - 1) \in Fin$
4	2 3	eqeltrdi	$⊢ (M \in ℤ \land N \in ℤ) \to (M ..^N) \in Fin$
5		fzof	$⊢ ..^: ℤ \times ℤ ⟶ 𝒫 ℤ$
6	5	fdmi	$⊢ dom ..^= ℤ \times ℤ$
7	6	ndmov	$⊢ \neg (M \in ℤ \land N \in ℤ) \to (M ..^N) = \emptyset$
8		0fin	$⊢ \emptyset \in Fin$
9	7 8	eqeltrdi	$⊢ \neg (M \in ℤ \land N \in ℤ) \to (M ..^N) \in Fin$
10	4 9	pm2.61i	$⊢ (M ..^N) \in Fin$

Metamath Proof Explorer