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 ) )