Theorem sqrtf

Description: Mapping domain and codomain of the square root function. (Contributed by Mario Carneiro, 13-Sep-2015)

	Ref	Expression
Assertion	sqrtf	|- sqrt : CC --> CC

Proof

Step	Hyp	Ref	Expression
1		riotaex	|- ( iota_ y e. CC ( ( y ^ 2 ) = x /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) e. _V
2		df-sqrt	|- sqrt = ( x e. CC |-> ( iota_ y e. CC ( ( y ^ 2 ) = x /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) )
3	1 2	fnmpti	|- sqrt Fn CC
4		sqrtcl	|- ( x e. CC -> ( sqrt ` x ) e. CC )
5	4	rgen	|- A. x e. CC ( sqrt ` x ) e. CC
6		ffnfv	|- ( sqrt : CC --> CC <-> ( sqrt Fn CC /\ A. x e. CC ( sqrt ` x ) e. CC ) )
7	3 5 6	mpbir2an	|- sqrt : CC --> CC