Theorem sqrtf

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

	Ref	Expression
Assertion	sqrtf	⊢ √ : ℂ ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		riotaex	⊢ ( ℩ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑥 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ∈ V
2		df-sqrt	⊢ √ = ( 𝑥 ∈ ℂ ↦ ( ℩ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑥 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) )
3	1 2	fnmpti	⊢ √ Fn ℂ
4		sqrtcl	⊢ ( 𝑥 ∈ ℂ → ( √ ‘ 𝑥 ) ∈ ℂ )
5	4	rgen	⊢ ∀ 𝑥 ∈ ℂ ( √ ‘ 𝑥 ) ∈ ℂ
6		ffnfv	⊢ ( √ : ℂ ⟶ ℂ ↔ ( √ Fn ℂ ∧ ∀ 𝑥 ∈ ℂ ( √ ‘ 𝑥 ) ∈ ℂ ) )
7	3 5 6	mpbir2an	⊢ √ : ℂ ⟶ ℂ