Description: Lower dimension axiom for one dimension. In dimension at least 1, there are at least two distinct points. The condition "the space is of dimension 1 or more" is written here as 2 <_ ( #P ) to avoid a new definition, but a different convention could be chosen. (Contributed by Thierry Arnoux, 23-Mar-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | tglowdim1.p | |- P = ( Base ` G ) |
|
| tglowdim1.d | |- .- = ( dist ` G ) |
||
| tglowdim1.i | |- I = ( Itv ` G ) |
||
| tglowdim1.g | |- ( ph -> G e. TarskiG ) |
||
| tglowdim1.1 | |- ( ph -> 2 <_ ( # ` P ) ) |
||
| Assertion | tglowdim1 | |- ( ph -> E. x e. P E. y e. P x =/= y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tglowdim1.p | |- P = ( Base ` G ) |
|
| 2 | tglowdim1.d | |- .- = ( dist ` G ) |
|
| 3 | tglowdim1.i | |- I = ( Itv ` G ) |
|
| 4 | tglowdim1.g | |- ( ph -> G e. TarskiG ) |
|
| 5 | tglowdim1.1 | |- ( ph -> 2 <_ ( # ` P ) ) |
|
| 6 | 1 | fvexi | |- P e. _V |
| 7 | hashge2el2dif | |- ( ( P e. _V /\ 2 <_ ( # ` P ) ) -> E. x e. P E. y e. P x =/= y ) |
|
| 8 | 6 5 7 | sylancr | |- ( ph -> E. x e. P E. y e. P x =/= y ) |