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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	axtrkge.d	⊢ − = ( dist ‘ 𝐺 )
	axtrkge.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	axtglowdim2.v	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	axtglowdim2.g	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
Assertion	axtglowdim2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		axtrkge.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		axtrkge.d	⊢ − = ( dist ‘ 𝐺 )
3		axtrkge.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		axtglowdim2.v	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5		axtglowdim2.g	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
6	1 2 3	istrkg2ld	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 DimTarskiG≥ 2 ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
7	4 6	syl	⊢ ( 𝜑 → ( 𝐺 DimTarskiG≥ 2 ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
8	5 7	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )