Metamath Proof Explorer

Theorem tncp

Description: In any planar incidence geometry, there exist three non-collinear points. (Contributed by FL, 3-Aug-2009)

Ref Expression
Hypothesis tncp.1 ⊢P=⋃G
Assertion tncp ⊢G∈Plig→∃a∈P∃b∈P∃c∈P∀l∈G¬a∈l∧b∈l∧c∈l

Proof

Step Hyp Ref Expression
1 tncp.1 ⊢P=⋃G
2 1 isplig ⊢G∈Plig→G∈Plig↔∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l∧∀l∈G∃a∈P∃b∈Pa≠b∧a∈l∧b∈l∧∃a∈P∃b∈P∃c∈P∀l∈G¬a∈l∧b∈l∧c∈l
3 2 ibi ⊢G∈Plig→∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l∧∀l∈G∃a∈P∃b∈Pa≠b∧a∈l∧b∈l∧∃a∈P∃b∈P∃c∈P∀l∈G¬a∈l∧b∈l∧c∈l
4 3 simp3d ⊢G∈Plig→∃a∈P∃b∈P∃c∈P∀l∈G¬a∈l∧b∈l∧c∈l