Theorem cjf

Description: Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	cjf	⊢ ∗ : ℂ ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		df-cj	⊢ ∗ = ( 𝑥 ∈ ℂ ↦ ( ℩ 𝑦 ∈ ℂ ( ( 𝑥 + 𝑦 ) ∈ ℝ ∧ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ ) ) )
2		cju	⊢ ( 𝑥 ∈ ℂ → ∃! 𝑦 ∈ ℂ ( ( 𝑥 + 𝑦 ) ∈ ℝ ∧ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ ) )
3		riotacl	⊢ ( ∃! 𝑦 ∈ ℂ ( ( 𝑥 + 𝑦 ) ∈ ℝ ∧ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ ) → ( ℩ 𝑦 ∈ ℂ ( ( 𝑥 + 𝑦 ) ∈ ℝ ∧ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ ) ) ∈ ℂ )
4	2 3	syl	⊢ ( 𝑥 ∈ ℂ → ( ℩ 𝑦 ∈ ℂ ( ( 𝑥 + 𝑦 ) ∈ ℝ ∧ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ ) ) ∈ ℂ )
5	1 4	fmpti	⊢ ∗ : ℂ ⟶ ℂ