Theorem tglowdim1

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={\mathrm{Base}}_G$$
	tglowdim1.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tglowdim1.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tglowdim1.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tglowdim1.1	$$⊢\phi \to 2\le \left|P\right|$$
Assertion	tglowdim1	$$⊢\phi \to \exists x\in P\exists y\in Px\ne y$$

Proof

Step	Hyp	Ref	Expression
1		tglowdim1.p	$$⊢P={\mathrm{Base}}_G$$
2		tglowdim1.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tglowdim1.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tglowdim1.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tglowdim1.1	$$⊢\phi \to 2\le \left|P\right|$$
6	1	fvexi	$$⊢P\in \mathrm{V}$$
7		hashge2el2dif	$$⊢\left(P\in \mathrm{V}\wedge 2\le \left|P\right|\right)\to \exists x\in P\exists y\in Px\ne y$$
8	6 5 7	sylancr	$$⊢\phi \to \exists x\in P\exists y\in Px\ne y$$