i1ff

Description: A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014)

		Ref	Expression
	Assertion	i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$

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	simp1d	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$

Metamath Proof Explorer