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_ CC -> ( C^n ` S ) Fn NN0 )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( CC ^pm S ) e. _V
2 1 rabex 
 |-  { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } e. _V
3 eqid 
 |-  ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) = ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } )
4 2 3 fnmpti 
 |-  ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) Fn NN0
5 cpnfval 
 |-  ( S C_ CC -> ( C^n ` S ) = ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) )
6 5 fneq1d 
 |-  ( S C_ CC -> ( ( C^n ` S ) Fn NN0 <-> ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) Fn NN0 ) )
7 4 6 mpbiri 
 |-  ( S C_ CC -> ( C^n ` S ) Fn NN0 )