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 )