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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tglowdim1.d	⊢ − = ( dist ‘ 𝐺 )
	tglowdim1.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglowdim1.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglowdim1.1	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
Assertion	tglowdim1	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝑥 ≠ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		tglowdim1.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tglowdim1.d	⊢ − = ( dist ‘ 𝐺 )
3		tglowdim1.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tglowdim1.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglowdim1.1	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
6	1	fvexi	⊢ 𝑃 ∈ V
7		hashge2el2dif	⊢ ( ( 𝑃 ∈ V ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝑥 ≠ 𝑦 )
8	6 5 7	sylancr	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 𝑥 ≠ 𝑦 )