Metamath Proof Explorer

Theorem i1ff

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

Ref Expression
Assertion i1ff ⊢ F ∈ dom ⁡ ∫ 1 → F : ℝ ⟶ ℝ

Proof

Step Hyp Ref Expression
1 isi1f ⊢ F ∈ dom ⁡ ∫ 1 ↔ F ∈ MblFn ∧ F : ℝ ⟶ ℝ ∧ ran ⁡ F ∈ Fin ∧ vol ⁡ F -1 ℝ ∖ 0 ∈ ℝ
2 1 simprbi ⊢ F ∈ dom ⁡ ∫ 1 → F : ℝ ⟶ ℝ ∧ ran ⁡ F ∈ Fin ∧ vol ⁡ F -1 ℝ ∖ 0 ∈ ℝ
3 2 simp1d ⊢ F ∈ dom ⁡ ∫ 1 → F : ℝ ⟶ ℝ