Metamath Proof Explorer

Theorem axlowdimlem10

Description: Lemma for axlowdim . Set up a family of points in Euclidean space. (Contributed by Scott Fenton, 21-Apr-2013)

Ref Expression
Hypothesis axlowdimlem10.1 
|- Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
Assertion axlowdimlem10 
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> Q e. ( EE ` N ) )

Proof

Step Hyp Ref Expression
1 axlowdimlem10.1 
 |-  Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
2 ovex 
 |-  ( I + 1 ) e. _V
3 1ex 
 |-  1 e. _V
4 2 3 f1osn 
 |-  { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } -1-1-onto-> { 1 }
5 f1of 
 |-  ( { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } -1-1-onto-> { 1 } -> { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } --> { 1 } )
6 4 5 ax-mp 
 |-  { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } --> { 1 }
7 c0ex 
 |-  0 e. _V
8 7 fconst 
 |-  ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) : ( ( 1 ... N ) \ { ( I + 1 ) } ) --> { 0 }
9 6 8 pm3.2i 
 |-  ( { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } --> { 1 } /\ ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) : ( ( 1 ... N ) \ { ( I + 1 ) } ) --> { 0 } )
10 disjdif 
 |-  ( { ( I + 1 ) } i^i ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = (/)
11 fun 
 |-  ( ( ( { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } --> { 1 } /\ ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) : ( ( 1 ... N ) \ { ( I + 1 ) } ) --> { 0 } ) /\ ( { ( I + 1 ) } i^i ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = (/) ) -> ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } ) )
12 9 10 11 mp2an 
 |-  ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } )
13 1 feq1i 
 |-  ( Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } ) <-> ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } ) )
14 12 13 mpbir 
 |-  Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } )
15 1re 
 |-  1 e. RR
16 snssi 
 |-  ( 1 e. RR -> { 1 } C_ RR )
17 15 16 ax-mp 
 |-  { 1 } C_ RR
18 0re 
 |-  0 e. RR
19 snssi 
 |-  ( 0 e. RR -> { 0 } C_ RR )
20 18 19 ax-mp 
 |-  { 0 } C_ RR
21 17 20 unssi 
 |-  ( { 1 } u. { 0 } ) C_ RR
22 fss 
 |-  ( ( Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } ) /\ ( { 1 } u. { 0 } ) C_ RR ) -> Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> RR )
23 14 21 22 mp2an 
 |-  Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> RR
24 fznatpl1 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( I + 1 ) e. ( 1 ... N ) )
25 24 snssd 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> { ( I + 1 ) } C_ ( 1 ... N ) )
26 undif 
 |-  ( { ( I + 1 ) } C_ ( 1 ... N ) <-> ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = ( 1 ... N ) )
27 25 26 sylib 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = ( 1 ... N ) )
28 27 feq2d 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> RR <-> Q : ( 1 ... N ) --> RR ) )
29 23 28 mpbii 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> Q : ( 1 ... N ) --> RR )
30 elee 
 |-  ( N e. NN -> ( Q e. ( EE ` N ) <-> Q : ( 1 ... N ) --> RR ) )
31 30 adantr 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( Q e. ( EE ` N ) <-> Q : ( 1 ... N ) --> RR ) )
32 29 31 mpbird 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> Q e. ( EE ` N ) )