Metamath Proof Explorer

Theorem i1frn

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

Ref Expression
Assertion i1frn ⊢ F ∈ dom ⁡ ∫ 1 → ran ⁡ F ∈ Fin

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 simp2d ⊢ F ∈ dom ⁡ ∫ 1 → ran ⁡ F ∈ Fin