Theorem tglowdim1i

Description: Lower dimension axiom for one dimension. (Contributed by Thierry Arnoux, 28-May-2019)

	Ref	Expression
Hypotheses	tglowdim1.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tglowdim1.d	⊢ − = ( dist ‘ 𝐺 )
	tglowdim1.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglowdim1.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglowdim1.1	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
	tglowdim1i.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
Assertion	tglowdim1i	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 𝑋 ≠ 𝑦 )

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		tglowdim1i.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
7	4	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) → 𝐺 ∈ TarskiG )
8	5	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
9	1 2 3 7 8	tglowdim1	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 𝑎 ≠ 𝑏 )
10		eqeq2	⊢ ( 𝑦 = 𝑎 → ( 𝑋 = 𝑦 ↔ 𝑋 = 𝑎 ) )
11		simpllr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 )
12		simplr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝑎 ∈ 𝑃 )
13	10 11 12	rspcdva	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝑋 = 𝑎 )
14		eqeq2	⊢ ( 𝑦 = 𝑏 → ( 𝑋 = 𝑦 ↔ 𝑋 = 𝑏 ) )
15	14	rspccva	⊢ ( ( ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ∧ 𝑏 ∈ 𝑃 ) → 𝑋 = 𝑏 )
16	15	ad4ant24	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝑋 = 𝑏 )
17	13 16	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝑎 = 𝑏 )
18		nne	⊢ ( ¬ 𝑎 ≠ 𝑏 ↔ 𝑎 = 𝑏 )
19	17 18	sylibr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ¬ 𝑎 ≠ 𝑏 )
20	19	nrexdv	⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) ∧ 𝑎 ∈ 𝑃 ) → ¬ ∃ 𝑏 ∈ 𝑃 𝑎 ≠ 𝑏 )
21	20	nrexdv	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 ) → ¬ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 𝑎 ≠ 𝑏 )
22	9 21	pm2.65da	⊢ ( 𝜑 → ¬ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 )
23		rexnal	⊢ ( ∃ 𝑦 ∈ 𝑃 ¬ 𝑋 = 𝑦 ↔ ¬ ∀ 𝑦 ∈ 𝑃 𝑋 = 𝑦 )
24	22 23	sylibr	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ¬ 𝑋 = 𝑦 )
25		df-ne	⊢ ( 𝑋 ≠ 𝑦 ↔ ¬ 𝑋 = 𝑦 )
26	25	rexbii	⊢ ( ∃ 𝑦 ∈ 𝑃 𝑋 ≠ 𝑦 ↔ ∃ 𝑦 ∈ 𝑃 ¬ 𝑋 = 𝑦 )
27	24 26	sylibr	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 𝑋 ≠ 𝑦 )