Metamath Proof Explorer

Theorem axlowdimlem7

Description: Lemma for axlowdim . Set up a point in Euclidean space. (Contributed by Scott Fenton, 29-Jun-2013)

Ref Expression
Hypothesis axlowdimlem7.1 
|- P = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
Assertion axlowdimlem7 
|- ( N e. ( ZZ>= ` 3 ) -> P e. ( EE ` N ) )

Proof

Step Hyp Ref Expression
1 axlowdimlem7.1 
 |-  P = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
2 eqid 
 |-  { <. 3 , -u 1 >. } = { <. 3 , -u 1 >. }
3 3ex 
 |-  3 e. _V
4 negex 
 |-  -u 1 e. _V
5 3 4 fsn 
 |-  ( { <. 3 , -u 1 >. } : { 3 } --> { -u 1 } <-> { <. 3 , -u 1 >. } = { <. 3 , -u 1 >. } )
6 2 5 mpbir 
 |-  { <. 3 , -u 1 >. } : { 3 } --> { -u 1 }
7 neg1rr 
 |-  -u 1 e. RR
8 snssi 
 |-  ( -u 1 e. RR -> { -u 1 } C_ RR )
9 7 8 ax-mp 
 |-  { -u 1 } C_ RR
10 fss 
 |-  ( ( { <. 3 , -u 1 >. } : { 3 } --> { -u 1 } /\ { -u 1 } C_ RR ) -> { <. 3 , -u 1 >. } : { 3 } --> RR )
11 6 9 10 mp2an 
 |-  { <. 3 , -u 1 >. } : { 3 } --> RR
12 0re 
 |-  0 e. RR
13 12 fconst6 
 |-  ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) : ( ( 1 ... N ) \ { 3 } ) --> RR
14 11 13 pm3.2i 
 |-  ( { <. 3 , -u 1 >. } : { 3 } --> RR /\ ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) : ( ( 1 ... N ) \ { 3 } ) --> RR )
15 disjdif 
 |-  ( { 3 } i^i ( ( 1 ... N ) \ { 3 } ) ) = (/)
16 fun2 
 |-  ( ( ( { <. 3 , -u 1 >. } : { 3 } --> RR /\ ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) : ( ( 1 ... N ) \ { 3 } ) --> RR ) /\ ( { 3 } i^i ( ( 1 ... N ) \ { 3 } ) ) = (/) ) -> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) : ( { 3 } u. ( ( 1 ... N ) \ { 3 } ) ) --> RR )
17 14 15 16 mp2an 
 |-  ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) : ( { 3 } u. ( ( 1 ... N ) \ { 3 } ) ) --> RR
18 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
19 1le3 
 |-  1 <_ 3
20 18 19 jctil 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 1 <_ 3 /\ 3 <_ N ) )
21 3z 
 |-  3 e. ZZ
22 1z 
 |-  1 e. ZZ
23 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
24 elfz 
 |-  ( ( 3 e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( 3 e. ( 1 ... N ) <-> ( 1 <_ 3 /\ 3 <_ N ) ) )
25 21 22 23 24 mp3an12i 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 3 e. ( 1 ... N ) <-> ( 1 <_ 3 /\ 3 <_ N ) ) )
26 20 25 mpbird 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 e. ( 1 ... N ) )
27 26 snssd 
 |-  ( N e. ( ZZ>= ` 3 ) -> { 3 } C_ ( 1 ... N ) )
28 undif 
 |-  ( { 3 } C_ ( 1 ... N ) <-> ( { 3 } u. ( ( 1 ... N ) \ { 3 } ) ) = ( 1 ... N ) )
29 27 28 sylib 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { 3 } u. ( ( 1 ... N ) \ { 3 } ) ) = ( 1 ... N ) )
30 29 feq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) : ( { 3 } u. ( ( 1 ... N ) \ { 3 } ) ) --> RR <-> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) : ( 1 ... N ) --> RR ) )
31 17 30 mpbii 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) : ( 1 ... N ) --> RR )
32 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
33 elee 
 |-  ( N e. NN -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) e. ( EE ` N ) <-> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) : ( 1 ... N ) --> RR ) )
34 32 33 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) e. ( EE ` N ) <-> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) : ( 1 ... N ) --> RR ) )
35 31 34 mpbird 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) e. ( EE ` N ) )
36 1 35 eqeltrid 
 |-  ( N e. ( ZZ>= ` 3 ) -> P e. ( EE ` N ) )