Theorem abvf

Description: An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abvf.a	|- A = ( AbsVal ` R )
	abvf.b	|- B = ( Base ` R )
Assertion	abvf	|- ( F e. A -> F : B --> RR )

Proof

Step	Hyp	Ref	Expression
1		abvf.a	|- A = ( AbsVal ` R )
2		abvf.b	|- B = ( Base ` R )
3	1 2	abvfge0	|- ( F e. A -> F : B --> ( 0 [,) +oo ) )
4		rge0ssre	|- ( 0 [,) +oo ) C_ RR
5		fss	|- ( ( F : B --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : B --> RR )
6	3 4 5	sylancl	|- ( F e. A -> F : B --> RR )