Theorem cjf

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

	Ref	Expression
Assertion	cjf	|- * : CC --> CC

Proof

Step	Hyp	Ref	Expression
1		df-cj	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
2		cju	|- ( x e. CC -> E! y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) )
3		riotacl	|- ( E! y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) -> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) e. CC )
4	2 3	syl	|- ( x e. CC -> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) e. CC )
5	1 4	fmpti	|- * : CC --> CC