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	⊢ 𝑃 = ∪ 𝐺
Assertion	tncp	⊢ ( 𝐺 ∈ Plig → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) )

Proof

Step	Hyp	Ref	Expression
1		tncp.1	⊢ 𝑃 = ∪ 𝐺
2	1	isplig	⊢ ( 𝐺 ∈ Plig → ( 𝐺 ∈ Plig ↔ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) ) )
3	2	ibi	⊢ ( 𝐺 ∈ Plig → ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) )
4	3	simp3d	⊢ ( 𝐺 ∈ Plig → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) )