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 Nx𝔼Ny𝔼Nxy

Proof

Step Hyp Ref Expression
1 1re 1
2 1 fconst6 1N×1:1N
3 elee N1N×1𝔼N1N×1:1N
4 2 3 mpbiri N1N×1𝔼N
5 0re 0
6 5 fconst6 1N×0:1N
7 elee N1N×0𝔼N1N×0:1N
8 6 7 mpbiri N1N×0𝔼N
9 ax-1ne0 10
10 9 neii ¬1=0
11 1ex 1V
12 11 sneqr 1=01=0
13 10 12 mto ¬1=0
14 elnnuz NN1
15 eluzfz1 N111N
16 14 15 sylbi N11N
17 16 ne0d N1N
18 rnxp 1Nran1N×1=1
19 17 18 syl Nran1N×1=1
20 rnxp 1Nran1N×0=0
21 17 20 syl Nran1N×0=0
22 19 21 eqeq12d Nran1N×1=ran1N×01=0
23 13 22 mtbiri N¬ran1N×1=ran1N×0
24 rneq 1N×1=1N×0ran1N×1=ran1N×0
25 23 24 nsyl N¬1N×1=1N×0
26 25 neqned N1N×11N×0
27 neeq1 x=1N×1xy1N×1y
28 neeq2 y=1N×01N×1y1N×11N×0
29 27 28 rspc2ev 1N×1𝔼N1N×0𝔼N1N×11N×0x𝔼Ny𝔼Nxy
30 4 8 26 29 syl3anc Nx𝔼Ny𝔼Nxy