This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fncpn

Description: The C^n object is a function. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion fncpn ⊢ S ⊆ ℂ → C n ⁡ S Fn ℕ 0

Proof

Step Hyp Ref Expression
1 ovex ⊢ ℂ ↑ 𝑝𝑚 S ∈ V
2 1 rabex ⊢ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ ∈ V
3 eqid ⊢ n ∈ ℕ 0 ⟼ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ = n ∈ ℕ 0 ⟼ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ
4 2 3 fnmpti ⊢ n ∈ ℕ 0 ⟼ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ Fn ℕ 0
5 cpnfval ⊢ S ⊆ ℂ → C n ⁡ S = n ∈ ℕ 0 ⟼ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ
6 5 fneq1d ⊢ S ⊆ ℂ → C n ⁡ S Fn ℕ 0 ↔ n ∈ ℕ 0 ⟼ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ Fn ℕ 0
7 4 6 mpbiri ⊢ S ⊆ ℂ → C n ⁡ S Fn ℕ 0