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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re | |
|
2 | 1 | fconst6 | |
3 | elee | |
|
4 | 2 3 | mpbiri | |
5 | 0re | |
|
6 | 5 | fconst6 | |
7 | elee | |
|
8 | 6 7 | mpbiri | |
9 | ax-1ne0 | |
|
10 | 9 | neii | |
11 | 1ex | |
|
12 | 11 | sneqr | |
13 | 10 12 | mto | |
14 | elnnuz | |
|
15 | eluzfz1 | |
|
16 | 14 15 | sylbi | |
17 | 16 | ne0d | |
18 | rnxp | |
|
19 | 17 18 | syl | |
20 | rnxp | |
|
21 | 17 20 | syl | |
22 | 19 21 | eqeq12d | |
23 | 13 22 | mtbiri | |
24 | rneq | |
|
25 | 23 24 | nsyl | |
26 | 25 | neqned | |
27 | neeq1 | |
|
28 | neeq2 | |
|
29 | 27 28 | rspc2ev | |
30 | 4 8 26 29 | syl3anc | |