Metamath Proof Explorer

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 ⊢ φ → G ∈ V
axtglowdim2.g ⊢ φ → G Dim 𝒢 ≥ 2
Assertion axtglowdim2 ⊢ φ → ∃ x ∈ P ∃ y ∈ P ∃ z ∈ P ¬ z ∈ x I y ∨ x ∈ z I y ∨ y ∈ 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 ⊢ φ → G ∈ V
5 axtglowdim2.g ⊢ φ → G Dim 𝒢 ≥ 2
6 1 2 3 istrkg2ld ⊢ G ∈ V → G Dim 𝒢 ≥ 2 ↔ ∃ x ∈ P ∃ y ∈ P ∃ z ∈ P ¬ z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
7 4 6 syl ⊢ φ → G Dim 𝒢 ≥ 2 ↔ ∃ x ∈ P ∃ y ∈ P ∃ z ∈ P ¬ z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
8 5 7 mpbid ⊢ φ → ∃ x ∈ P ∃ y ∈ P ∃ z ∈ P ¬ z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z