Metamath Proof Explorer

Theorem mptelee

Description: A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013)

Ref Expression
Assertion mptelee 
|- ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( A F B ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( A F B ) e. RR ) )

Proof

Step Hyp Ref Expression
1 elee 
 |-  ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( A F B ) ) e. ( EE ` N ) <-> ( k e. ( 1 ... N ) |-> ( A F B ) ) : ( 1 ... N ) --> RR ) )
2 ovex 
 |-  ( A F B ) e. _V
3 eqid 
 |-  ( k e. ( 1 ... N ) |-> ( A F B ) ) = ( k e. ( 1 ... N ) |-> ( A F B ) )
4 2 3 fnmpti 
 |-  ( k e. ( 1 ... N ) |-> ( A F B ) ) Fn ( 1 ... N )
5 df-f 
 |-  ( ( k e. ( 1 ... N ) |-> ( A F B ) ) : ( 1 ... N ) --> RR <-> ( ( k e. ( 1 ... N ) |-> ( A F B ) ) Fn ( 1 ... N ) /\ ran ( k e. ( 1 ... N ) |-> ( A F B ) ) C_ RR ) )
6 4 5 mpbiran 
 |-  ( ( k e. ( 1 ... N ) |-> ( A F B ) ) : ( 1 ... N ) --> RR <-> ran ( k e. ( 1 ... N ) |-> ( A F B ) ) C_ RR )
7 3 rnmpt 
 |-  ran ( k e. ( 1 ... N ) |-> ( A F B ) ) = { a | E. k e. ( 1 ... N ) a = ( A F B ) }
8 7 sseq1i 
 |-  ( ran ( k e. ( 1 ... N ) |-> ( A F B ) ) C_ RR <-> { a | E. k e. ( 1 ... N ) a = ( A F B ) } C_ RR )
9 abss 
 |-  ( { a | E. k e. ( 1 ... N ) a = ( A F B ) } C_ RR <-> A. a ( E. k e. ( 1 ... N ) a = ( A F B ) -> a e. RR ) )
10 nfre1 
 |-  F/ k E. k e. ( 1 ... N ) a = ( A F B )
11 nfv 
 |-  F/ k a e. RR
12 10 11 nfim 
 |-  F/ k ( E. k e. ( 1 ... N ) a = ( A F B ) -> a e. RR )
13 12 nfal 
 |-  F/ k A. a ( E. k e. ( 1 ... N ) a = ( A F B ) -> a e. RR )
14 r19.23v 
 |-  ( A. k e. ( 1 ... N ) ( a = ( A F B ) -> a e. RR ) <-> ( E. k e. ( 1 ... N ) a = ( A F B ) -> a e. RR ) )
15 14 albii 
 |-  ( A. a A. k e. ( 1 ... N ) ( a = ( A F B ) -> a e. RR ) <-> A. a ( E. k e. ( 1 ... N ) a = ( A F B ) -> a e. RR ) )
16 ralcom4 
 |-  ( A. k e. ( 1 ... N ) A. a ( a = ( A F B ) -> a e. RR ) <-> A. a A. k e. ( 1 ... N ) ( a = ( A F B ) -> a e. RR ) )
17 rsp 
 |-  ( A. k e. ( 1 ... N ) A. a ( a = ( A F B ) -> a e. RR ) -> ( k e. ( 1 ... N ) -> A. a ( a = ( A F B ) -> a e. RR ) ) )
18 2 clel2 
 |-  ( ( A F B ) e. RR <-> A. a ( a = ( A F B ) -> a e. RR ) )
19 17 18 syl6ibr 
 |-  ( A. k e. ( 1 ... N ) A. a ( a = ( A F B ) -> a e. RR ) -> ( k e. ( 1 ... N ) -> ( A F B ) e. RR ) )
20 16 19 sylbir 
 |-  ( A. a A. k e. ( 1 ... N ) ( a = ( A F B ) -> a e. RR ) -> ( k e. ( 1 ... N ) -> ( A F B ) e. RR ) )
21 15 20 sylbir 
 |-  ( A. a ( E. k e. ( 1 ... N ) a = ( A F B ) -> a e. RR ) -> ( k e. ( 1 ... N ) -> ( A F B ) e. RR ) )
22 13 21 ralrimi 
 |-  ( A. a ( E. k e. ( 1 ... N ) a = ( A F B ) -> a e. RR ) -> A. k e. ( 1 ... N ) ( A F B ) e. RR )
23 nfra1 
 |-  F/ k A. k e. ( 1 ... N ) ( A F B ) e. RR
24 rsp 
 |-  ( A. k e. ( 1 ... N ) ( A F B ) e. RR -> ( k e. ( 1 ... N ) -> ( A F B ) e. RR ) )
25 eleq1a 
 |-  ( ( A F B ) e. RR -> ( a = ( A F B ) -> a e. RR ) )
26 24 25 syl6 
 |-  ( A. k e. ( 1 ... N ) ( A F B ) e. RR -> ( k e. ( 1 ... N ) -> ( a = ( A F B ) -> a e. RR ) ) )
27 23 11 26 rexlimd 
 |-  ( A. k e. ( 1 ... N ) ( A F B ) e. RR -> ( E. k e. ( 1 ... N ) a = ( A F B ) -> a e. RR ) )
28 27 alrimiv 
 |-  ( A. k e. ( 1 ... N ) ( A F B ) e. RR -> A. a ( E. k e. ( 1 ... N ) a = ( A F B ) -> a e. RR ) )
29 22 28 impbii 
 |-  ( A. a ( E. k e. ( 1 ... N ) a = ( A F B ) -> a e. RR ) <-> A. k e. ( 1 ... N ) ( A F B ) e. RR )
30 9 29 bitri 
 |-  ( { a | E. k e. ( 1 ... N ) a = ( A F B ) } C_ RR <-> A. k e. ( 1 ... N ) ( A F B ) e. RR )
31 8 30 bitri 
 |-  ( ran ( k e. ( 1 ... N ) |-> ( A F B ) ) C_ RR <-> A. k e. ( 1 ... N ) ( A F B ) e. RR )
32 6 31 bitri 
 |-  ( ( k e. ( 1 ... N ) |-> ( A F B ) ) : ( 1 ... N ) --> RR <-> A. k e. ( 1 ... N ) ( A F B ) e. RR )
33 1 32 bitrdi 
 |-  ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( A F B ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( A F B ) e. RR ) )