i1frn

Description: A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014)

		Ref	Expression
	Assertion	i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$

Step	Hyp	Ref	Expression
1		isi1f	$⊢ F \in dom \int^{1} \leftrightarrow (F \in MblFn \land (F : ℝ ⟶ ℝ \land ran F \in Fin \land vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ))$
2	1	simprbi	$⊢ F \in dom \int^{1} \to (F : ℝ ⟶ ℝ \land ran F \in Fin \land vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ)$
3	2	simp2d	$⊢ F \in dom \int^{1} \to ran F \in Fin$

Metamath Proof Explorer