Metamath Proof Explorer

Theorem tglowdim2l

Description: Reformulation of the lower dimension axiom for dimension two. There exist three non-colinear points. Theorem 6.24 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 30-May-2019)

Ref Expression
Hypotheses tglineintmo.p ⊢ P = Base G
tglineintmo.i ⊢ I = Itv ⁡ G
tglineintmo.l ⊢ L = Line 𝒢 ⁡ G
tglineintmo.g ⊢ φ → G ∈ 𝒢 Tarski
tglowdim2l.1 ⊢ φ → G Dim 𝒢 ≥ 2
Assertion tglowdim2l ⊢ φ → ∃ a ∈ P ∃ b ∈ P ∃ c ∈ P ¬ c ∈ a L b ∨ a = b

Proof

Step Hyp Ref Expression
1 tglineintmo.p ⊢ P = Base G
2 tglineintmo.i ⊢ I = Itv ⁡ G
3 tglineintmo.l ⊢ L = Line 𝒢 ⁡ G
4 tglineintmo.g ⊢ φ → G ∈ 𝒢 Tarski
5 tglowdim2l.1 ⊢ φ → G Dim 𝒢 ≥ 2
6 eqid ⊢ dist ⁡ G = dist ⁡ G
7 1 6 2 4 5 axtglowdim2 ⊢ φ → ∃ a ∈ P ∃ b ∈ P ∃ c ∈ P ¬ c ∈ a I b ∨ a ∈ c I b ∨ b ∈ a I c
8 4 ad3antrrr ⊢ φ ∧ a ∈ P ∧ b ∈ P ∧ c ∈ P → G ∈ 𝒢 Tarski
9 simpllr ⊢ φ ∧ a ∈ P ∧ b ∈ P ∧ c ∈ P → a ∈ P
10 simplr ⊢ φ ∧ a ∈ P ∧ b ∈ P ∧ c ∈ P → b ∈ P
11 simpr ⊢ φ ∧ a ∈ P ∧ b ∈ P ∧ c ∈ P → c ∈ P
12 1 3 2 8 9 10 11 tgcolg ⊢ φ ∧ a ∈ P ∧ b ∈ P ∧ c ∈ P → c ∈ a L b ∨ a = b ↔ c ∈ a I b ∨ a ∈ c I b ∨ b ∈ a I c
13 12 notbid ⊢ φ ∧ a ∈ P ∧ b ∈ P ∧ c ∈ P → ¬ c ∈ a L b ∨ a = b ↔ ¬ c ∈ a I b ∨ a ∈ c I b ∨ b ∈ a I c
14 13 rexbidva ⊢ φ ∧ a ∈ P ∧ b ∈ P → ∃ c ∈ P ¬ c ∈ a L b ∨ a = b ↔ ∃ c ∈ P ¬ c ∈ a I b ∨ a ∈ c I b ∨ b ∈ a I c
15 14 rexbidva ⊢ φ ∧ a ∈ P → ∃ b ∈ P ∃ c ∈ P ¬ c ∈ a L b ∨ a = b ↔ ∃ b ∈ P ∃ c ∈ P ¬ c ∈ a I b ∨ a ∈ c I b ∨ b ∈ a I c
16 15 rexbidva ⊢ φ → ∃ a ∈ P ∃ b ∈ P ∃ c ∈ P ¬ c ∈ a L b ∨ a = b ↔ ∃ a ∈ P ∃ b ∈ P ∃ c ∈ P ¬ c ∈ a I b ∨ a ∈ c I b ∨ b ∈ a I c
17 7 16 mpbird ⊢ φ → ∃ a ∈ P ∃ b ∈ P ∃ c ∈ P ¬ c ∈ a L b ∨ a = b