sqrtf

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

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

Step	Hyp	Ref	Expression
1		riotaex	$⊢ (ι y \in ℂ \| (y^{2} = x \land 0 \leq ℜ (y) \land i y \notin ℝ^{+})) \in V$
2		df-sqrt	$⊢ \sqrt = (x \in ℂ ⟼ (ι y \in ℂ \| (y^{2} = x \land 0 \leq ℜ (y) \land i y \notin ℝ^{+})))$
3	1 2	fnmpti	$⊢ \sqrt Fn ℂ$
4		sqrtcl	$⊢ x \in ℂ \to \sqrt{x} \in ℂ$
5	4	rgen	$⊢ \forall x \in ℂ \sqrt{x} \in ℂ$
6		ffnfv	$⊢ \sqrt : ℂ ⟶ ℂ \leftrightarrow (\sqrt Fn ℂ \land \forall x \in ℂ \sqrt{x} \in ℂ)$
7	3 5 6	mpbir2an	$⊢ \sqrt : ℂ ⟶ ℂ$

Metamath Proof Explorer