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 )

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 )

Step

Hyp

Ref

Expression

 |-  ( F e. dom S.1 <-> ( F e. MblFn /\ ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) )

 |-  ( F e. dom S.1 -> ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) )

 |-  ( F e. dom S.1 -> ran F e. Fin )