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 ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l ∧ ∀ l ∈ G ∃ a ∈ P ∃ b ∈ P a ≠ 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 ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l ∧ ∀ l ∈ G ∃ a ∈ P ∃ b ∈ P a ≠ 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