Metamath Proof Explorer

Theorem axlowdim1

Description: The lower dimension axiom for one dimension. In any dimension, there are at least two distinct points. Theorem 3.13 of Schwabhauser p. 32, where it is derived from axlowdim2 . (Contributed by Scott Fenton, 22-Apr-2013)

Ref Expression
Assertion axlowdim1 
|- ( N e. NN -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) x =/= y )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 1 fconst6 
 |-  ( ( 1 ... N ) X. { 1 } ) : ( 1 ... N ) --> RR
3 elee 
 |-  ( N e. NN -> ( ( ( 1 ... N ) X. { 1 } ) e. ( EE ` N ) <-> ( ( 1 ... N ) X. { 1 } ) : ( 1 ... N ) --> RR ) )
4 2 3 mpbiri 
 |-  ( N e. NN -> ( ( 1 ... N ) X. { 1 } ) e. ( EE ` N ) )
5 0re 
 |-  0 e. RR
6 5 fconst6 
 |-  ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> RR
7 elee 
 |-  ( N e. NN -> ( ( ( 1 ... N ) X. { 0 } ) e. ( EE ` N ) <-> ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> RR ) )
8 6 7 mpbiri 
 |-  ( N e. NN -> ( ( 1 ... N ) X. { 0 } ) e. ( EE ` N ) )
9 ax-1ne0 
 |-  1 =/= 0
10 9 neii 
 |-  -. 1 = 0
11 1ex 
 |-  1 e. _V
12 11 sneqr 
 |-  ( { 1 } = { 0 } -> 1 = 0 )
13 10 12 mto 
 |-  -. { 1 } = { 0 }
14 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
15 eluzfz1 
 |-  ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
16 14 15 sylbi 
 |-  ( N e. NN -> 1 e. ( 1 ... N ) )
17 16 ne0d 
 |-  ( N e. NN -> ( 1 ... N ) =/= (/) )
18 rnxp 
 |-  ( ( 1 ... N ) =/= (/) -> ran ( ( 1 ... N ) X. { 1 } ) = { 1 } )
19 17 18 syl 
 |-  ( N e. NN -> ran ( ( 1 ... N ) X. { 1 } ) = { 1 } )
20 rnxp 
 |-  ( ( 1 ... N ) =/= (/) -> ran ( ( 1 ... N ) X. { 0 } ) = { 0 } )
21 17 20 syl 
 |-  ( N e. NN -> ran ( ( 1 ... N ) X. { 0 } ) = { 0 } )
22 19 21 eqeq12d 
 |-  ( N e. NN -> ( ran ( ( 1 ... N ) X. { 1 } ) = ran ( ( 1 ... N ) X. { 0 } ) <-> { 1 } = { 0 } ) )
23 13 22 mtbiri 
 |-  ( N e. NN -> -. ran ( ( 1 ... N ) X. { 1 } ) = ran ( ( 1 ... N ) X. { 0 } ) )
24 rneq 
 |-  ( ( ( 1 ... N ) X. { 1 } ) = ( ( 1 ... N ) X. { 0 } ) -> ran ( ( 1 ... N ) X. { 1 } ) = ran ( ( 1 ... N ) X. { 0 } ) )
25 23 24 nsyl 
 |-  ( N e. NN -> -. ( ( 1 ... N ) X. { 1 } ) = ( ( 1 ... N ) X. { 0 } ) )
26 25 neqned 
 |-  ( N e. NN -> ( ( 1 ... N ) X. { 1 } ) =/= ( ( 1 ... N ) X. { 0 } ) )
27 neeq1 
 |-  ( x = ( ( 1 ... N ) X. { 1 } ) -> ( x =/= y <-> ( ( 1 ... N ) X. { 1 } ) =/= y ) )
28 neeq2 
 |-  ( y = ( ( 1 ... N ) X. { 0 } ) -> ( ( ( 1 ... N ) X. { 1 } ) =/= y <-> ( ( 1 ... N ) X. { 1 } ) =/= ( ( 1 ... N ) X. { 0 } ) ) )
29 27 28 rspc2ev 
 |-  ( ( ( ( 1 ... N ) X. { 1 } ) e. ( EE ` N ) /\ ( ( 1 ... N ) X. { 0 } ) e. ( EE ` N ) /\ ( ( 1 ... N ) X. { 1 } ) =/= ( ( 1 ... N ) X. { 0 } ) ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) x =/= y )
30 4 8 26 29 syl3anc 
 |-  ( N e. NN -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) x =/= y )