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	$$⊢*=\left(x\in ℂ⟼\left(\iota y\in ℂ|\left(x+y\in ℝ\wedge \mathrm{i}\left(x-y\right)\in ℝ\right)\right)\right)$$
2		cju	$$⊢x\in ℂ\to \exists !y\in ℂ\left(x+y\in ℝ\wedge \mathrm{i}\left(x-y\right)\in ℝ\right)$$
3		riotacl	$$⊢\exists !y\in ℂ\left(x+y\in ℝ\wedge \mathrm{i}\left(x-y\right)\in ℝ\right)\to \left(\iota y\in ℂ|\left(x+y\in ℝ\wedge \mathrm{i}\left(x-y\right)\in ℝ\right)\right)\in ℂ$$
4	2 3	syl	$$⊢x\in ℂ\to \left(\iota y\in ℂ|\left(x+y\in ℝ\wedge \mathrm{i}\left(x-y\right)\in ℝ\right)\right)\in ℂ$$
5	1 4	fmpti	$$⊢*:ℂ⟶ℂ$$