Theorem tglowdim1i

Description: Lower dimension axiom for one dimension. (Contributed by Thierry Arnoux, 28-May-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|$$
	tglowdim1i.1	$$⊢\phi \to X\in P$$
Assertion	tglowdim1i	$$⊢\phi \to \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		tglowdim1i.1	$$⊢\phi \to X\in P$$
7	4	adantr	$$⊢\left(\phi \wedge \forall y\in PX=y\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
8	5	adantr	$$⊢\left(\phi \wedge \forall y\in PX=y\right)\to 2\le \left|P\right|$$
9	1 2 3 7 8	tglowdim1	$$⊢\left(\phi \wedge \forall y\in PX=y\right)\to \exists a\in P\exists b\in Pa\ne b$$
10		eqeq2	$$⊢y=a\to \left(X=y\leftrightarrow X=a\right)$$
11		simpllr	$$⊢\left(\left(\left(\phi \wedge \forall y\in PX=y\right)\wedge a\in P\right)\wedge b\in P\right)\to \forall y\in PX=y$$
12		simplr	$$⊢\left(\left(\left(\phi \wedge \forall y\in PX=y\right)\wedge a\in P\right)\wedge b\in P\right)\to a\in P$$
13	10 11 12	rspcdva	$$⊢\left(\left(\left(\phi \wedge \forall y\in PX=y\right)\wedge a\in P\right)\wedge b\in P\right)\to X=a$$
14		eqeq2	$$⊢y=b\to \left(X=y\leftrightarrow X=b\right)$$
15	14	rspccva	$$⊢\left(\forall y\in PX=y\wedge b\in P\right)\to X=b$$
16	15	ad4ant24	$$⊢\left(\left(\left(\phi \wedge \forall y\in PX=y\right)\wedge a\in P\right)\wedge b\in P\right)\to X=b$$
17	13 16	eqtr3d	$$⊢\left(\left(\left(\phi \wedge \forall y\in PX=y\right)\wedge a\in P\right)\wedge b\in P\right)\to a=b$$
18		nne	$$⊢\neg a\ne b\leftrightarrow a=b$$
19	17 18	sylibr	$$⊢\left(\left(\left(\phi \wedge \forall y\in PX=y\right)\wedge a\in P\right)\wedge b\in P\right)\to \neg a\ne b$$
20	19	nrexdv	$$⊢\left(\left(\phi \wedge \forall y\in PX=y\right)\wedge a\in P\right)\to \neg \exists b\in Pa\ne b$$
21	20	nrexdv	$$⊢\left(\phi \wedge \forall y\in PX=y\right)\to \neg \exists a\in P\exists b\in Pa\ne b$$
22	9 21	pm2.65da	$$⊢\phi \to \neg \forall y\in PX=y$$
23		rexnal	$$⊢\exists y\in P\neg X=y\leftrightarrow \neg \forall y\in PX=y$$
24	22 23	sylibr	$$⊢\phi \to \exists y\in P\neg X=y$$
25		df-ne	$$⊢X\ne y\leftrightarrow \neg X=y$$
26	25	rexbii	$$⊢\exists y\in PX\ne y\leftrightarrow \exists y\in P\neg X=y$$
27	24 26	sylibr	$$⊢\phi \to \exists y\in PX\ne y$$