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=BaseG
tglineintmo.i ⊢I=Itv⁡G
tglineintmo.l ⊢L=Line𝒢⁡G
tglineintmo.g ⊢φ→G∈𝒢Tarski
tglowdim2l.1 ⊢φ→GDim𝒢≥2
Assertion tglowdim2l ⊢φ→∃a∈P∃b∈P∃c∈P¬c∈aLb∨a=b

Proof

Step Hyp Ref Expression
1 tglineintmo.p ⊢P=BaseG
2 tglineintmo.i ⊢I=Itv⁡G
3 tglineintmo.l ⊢L=Line𝒢⁡G
4 tglineintmo.g ⊢φ→G∈𝒢Tarski
5 tglowdim2l.1 ⊢φ→GDim𝒢≥2
6 eqid ⊢dist⁡G=dist⁡G
7 1 6 2 4 5 axtglowdim2 ⊢φ→∃a∈P∃b∈P∃c∈P¬c∈aIb∨a∈cIb∨b∈aIc
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∈aLb∨a=b↔c∈aIb∨a∈cIb∨b∈aIc
13 12 notbid ⊢φ∧a∈P∧b∈P∧c∈P→¬c∈aLb∨a=b↔¬c∈aIb∨a∈cIb∨b∈aIc
14 13 rexbidva ⊢φ∧a∈P∧b∈P→∃c∈P¬c∈aLb∨a=b↔∃c∈P¬c∈aIb∨a∈cIb∨b∈aIc
15 14 rexbidva ⊢φ∧a∈P→∃b∈P∃c∈P¬c∈aLb∨a=b↔∃b∈P∃c∈P¬c∈aIb∨a∈cIb∨b∈aIc
16 15 rexbidva ⊢φ→∃a∈P∃b∈P∃c∈P¬c∈aLb∨a=b↔∃a∈P∃b∈P∃c∈P¬c∈aIb∨a∈cIb∨b∈aIc
17 7 16 mpbird ⊢φ→∃a∈P∃b∈P∃c∈P¬c∈aLb∨a=b