Theorem imf

Description: Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007) (Revised by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	imf	|- Im : CC --> RR

Proof

Step	Hyp	Ref	Expression
1		df-im	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
2		imval	|- ( x e. CC -> ( Im ` x ) = ( Re ` ( x / _i ) ) )
3		imcl	|- ( x e. CC -> ( Im ` x ) e. RR )
4	2 3	eqeltrrd	|- ( x e. CC -> ( Re ` ( x / _i ) ) e. RR )
5	1 4	fmpti	|- Im : CC --> RR