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 ) |
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 ) |