Theorem ref

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

	Ref	Expression
Assertion	ref	⊢ ℜ : ℂ ⟶ ℝ

Proof

Step	Hyp	Ref	Expression
1		df-re	⊢ ℜ = ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 + ( ∗ ‘ 𝑥 ) ) / 2 ) )
2		reval	⊢ ( 𝑥 ∈ ℂ → ( ℜ ‘ 𝑥 ) = ( ( 𝑥 + ( ∗ ‘ 𝑥 ) ) / 2 ) )
3		recl	⊢ ( 𝑥 ∈ ℂ → ( ℜ ‘ 𝑥 ) ∈ ℝ )
4	2 3	eqeltrrd	⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 + ( ∗ ‘ 𝑥 ) ) / 2 ) ∈ ℝ )
5	1 4	fmpti	⊢ ℜ : ℂ ⟶ ℝ