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	$⊢ (M \dots N) \in Fin$

Proof

Step	Hyp	Ref	Expression
1		0fi	$⊢ \emptyset \in Fin$
2		eleq1	$⊢ (M \dots N) = \emptyset \to ((M \dots N) \in Fin \leftrightarrow \emptyset \in Fin)$
3	1 2	mpbiri	$⊢ (M \dots N) = \emptyset \to (M \dots N) \in Fin$
4		fzn0	$⊢ (M \dots N) \neq \emptyset \leftrightarrow N \in ℤ_{\geq M}$
5		onfin2	$⊢ ω = On \cap Fin$
6		inss2	$⊢ On \cap Fin \subseteq Fin$
7	5 6	eqsstri	$⊢ ω \subseteq Fin$
8		eqid	$⊢ {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
9	8	hashgf1o	$⊢ ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0}$
10		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
11		uznn0sub	$⊢ N + 1 \in ℤ_{\geq M} \to N + 1 - M \in ℕ_{0}$
12	10 11	syl	$⊢ N \in ℤ_{\geq M} \to N + 1 - M \in ℕ_{0}$
13		f1ocnvdm	$⊢ (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0} \land N + 1 - M \in ℕ_{0}) \to {({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})}^{-1} (N + 1 - M) \in ω$
14	9 12 13	sylancr	$⊢ N \in ℤ_{\geq M} \to {({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})}^{-1} (N + 1 - M) \in ω$
15	7 14	sselid	$⊢ N \in ℤ_{\geq M} \to {({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})}^{-1} (N + 1 - M) \in Fin$
16	8	fzen2	$⊢ N \in ℤ_{\geq M} \to (M \dots N) \approx {({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})}^{-1} (N + 1 - M)$
17		enfii	$⊢ ({({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})}^{-1} (N + 1 - M) \in Fin \land (M \dots N) \approx {({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})}^{-1} (N + 1 - M)) \to (M \dots N) \in Fin$
18	15 16 17	syl2anc	$⊢ N \in ℤ_{\geq M} \to (M \dots N) \in Fin$
19	4 18	sylbi	$⊢ (M \dots N) \neq \emptyset \to (M \dots N) \in Fin$
20	3 19	pm2.61ine	$⊢ (M \dots N) \in Fin$

Metamath Proof Explorer

Theorem fzfi

Proof