cjf

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

		Ref	Expression
	Assertion	cjf	$⊢ * : ℂ ⟶ ℂ$

Step	Hyp	Ref	Expression
1		df-cj	$⊢ * = (x \in ℂ ⟼ (ι y \in ℂ \| (x + y \in ℝ \land i (x - y) \in ℝ)))$
2		cju	$⊢ x \in ℂ \to \exists! y \in ℂ (x + y \in ℝ \land i (x - y) \in ℝ)$
3		riotacl	$⊢ \exists! y \in ℂ (x + y \in ℝ \land i (x - y) \in ℝ) \to (ι y \in ℂ \| (x + y \in ℝ \land i (x - y) \in ℝ)) \in ℂ$
4	2 3	syl	$⊢ x \in ℂ \to (ι y \in ℂ \| (x + y \in ℝ \land i (x - y) \in ℝ)) \in ℂ$
5	1 4	fmpti	$⊢ * : ℂ ⟶ ℂ$

Metamath Proof Explorer