Theorem axtglowdim2

Description: Lower dimension axiom for dimension 2, Axiom A8 of Schwabhauser p. 13. There exist 3 non-colinear points. (Contributed by Thierry Arnoux, 20-Nov-2019)

	Ref	Expression
Hypotheses	axtrkge.p	$$⊢P={\mathrm{Base}}_G$$
	axtrkge.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	axtrkge.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	axtglowdim2.v	$$⊢\phi \to G\in V$$
	axtglowdim2.g	$$⊢\phi \to G{\mathrm{Dim}}_{𝒢}\ge 2$$
Assertion	axtglowdim2	$$⊢\phi \to \exists x\in P\exists y\in P\exists z\in P\neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		axtrkge.p	$$⊢P={\mathrm{Base}}_G$$
2		axtrkge.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		axtrkge.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		axtglowdim2.v	$$⊢\phi \to G\in V$$
5		axtglowdim2.g	$$⊢\phi \to G{\mathrm{Dim}}_{𝒢}\ge 2$$
6	1 2 3	istrkg2ld	$$⊢G\in V\to \left(G{\mathrm{Dim}}_{𝒢}\ge 2\leftrightarrow \exists x\in P\exists y\in P\exists z\in P\neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)$$
7	4 6	syl	$$⊢\phi \to \left(G{\mathrm{Dim}}_{𝒢}\ge 2\leftrightarrow \exists x\in P\exists y\in P\exists z\in P\neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)$$
8	5 7	mpbid	$$⊢\phi \to \exists x\in P\exists y\in P\exists z\in P\neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)$$