Theorem sqrtf

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

	Ref	Expression
Assertion	sqrtf	$$⊢\surd :ℂ⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		riotaex	$$⊢\left(\iota y\in ℂ|\left(y^2=x\wedge 0\le \Re \left(y\right)\wedge \mathrm{i}y\notin {ℝ}^{+}\right)\right)\in \mathrm{V}$$
2		df-sqrt	$$⊢\surd =\left(x\in ℂ⟼\left(\iota y\in ℂ|\left(y^2=x\wedge 0\le \Re \left(y\right)\wedge \mathrm{i}y\notin {ℝ}^{+}\right)\right)\right)$$
3	1 2	fnmpti	$$⊢\surd Fnℂ$$
4		sqrtcl	$$⊢x\in ℂ\to \sqrt{x}\in ℂ$$
5	4	rgen	$$⊢\forall x\in ℂ\sqrt{x}\in ℂ$$
6		ffnfv	$$⊢\surd :ℂ⟶ℂ\leftrightarrow \left(\surd Fnℂ\wedge \forall x\in ℂ\sqrt{x}\in ℂ\right)$$
7	3 5 6	mpbir2an	$$⊢\surd :ℂ⟶ℂ$$