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 e. dom S.1 -> F : RR --> RR )

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	simp1d	\|- ( F e. dom S.1 -> F : RR --> RR )

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 -> F : RR --> RR )