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 = ( Base ` G )
	axtrkge.d	|- .- = ( dist ` G )
	axtrkge.i	|- I = ( Itv ` G )
	axtglowdim2.v	|- ( ph -> G e. V )
	axtglowdim2.g	|- ( ph -> G TarskiGDim>= 2 )
Assertion	axtglowdim2	|- ( ph -> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )

Proof

Step	Hyp	Ref	Expression
1		axtrkge.p	|- P = ( Base ` G )
2		axtrkge.d	|- .- = ( dist ` G )
3		axtrkge.i	|- I = ( Itv ` G )
4		axtglowdim2.v	|- ( ph -> G e. V )
5		axtglowdim2.g	|- ( ph -> G TarskiGDim>= 2 )
6	1 2 3	istrkg2ld	|- ( G e. V -> ( G TarskiGDim>= 2 <-> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
7	4 6	syl	|- ( ph -> ( G TarskiGDim>= 2 <-> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
8	5 7	mpbid	|- ( ph -> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )