Metamath Proof Explorer


Theorem i1frn

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

Ref Expression
Assertion i1frn
|- ( F e. dom S.1 -> ran F e. Fin )

Proof

Step Hyp Ref Expression
1 isi1f
 |-  ( F e. dom S.1 <-> ( F e. MblFn /\ ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) )
2 1 simprbi
 |-  ( F e. dom S.1 -> ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) )
3 2 simp2d
 |-  ( F e. dom S.1 -> ran F e. Fin )