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 ( 𝑆 ⊆ ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) Fn ℕ0 )

Proof

Step Hyp Ref Expression
1 ovex ⊢ ( ℂ ↑pm 𝑆 ) ∈ V
2 1 rabex ⊢ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ∈ V
3 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } )
4 2 3 fnmpti ⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) Fn ℕ0
5 cpnfval ⊢ ( 𝑆 ⊆ ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )
6 5 fneq1d ⊢ ( 𝑆 ⊆ ℂ → ( ( 𝓑C𝑛 ‘ 𝑆 ) Fn ℕ0 ↔ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) Fn ℕ0 ) )
7 4 6 mpbiri ⊢ ( 𝑆 ⊆ ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) Fn ℕ0 )