Theorem l2p

Description: For any line in a planar incidence geometry, there exist two different points on the line. (Contributed by AV, 28-Nov-2021)

	Ref	Expression
Hypothesis	l2p.1	⊢ 𝑃 = ∪ 𝐺
Assertion	l2p	⊢ ( ( 𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		l2p.1	⊢ 𝑃 = ∪ 𝐺
2	1	isplig	⊢ ( 𝐺 ∈ Plig → ( 𝐺 ∈ Plig ↔ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) ) )
3		eleq2	⊢ ( 𝑙 = 𝐿 → ( 𝑎 ∈ 𝑙 ↔ 𝑎 ∈ 𝐿 ) )
4		eleq2	⊢ ( 𝑙 = 𝐿 → ( 𝑏 ∈ 𝑙 ↔ 𝑏 ∈ 𝐿 ) )
5	3 4	3anbi23d	⊢ ( 𝑙 = 𝐿 → ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ↔ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿 ) ) )
6	5	2rexbidv	⊢ ( 𝑙 = 𝐿 → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿 ) ) )
7	6	rspccv	⊢ ( ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) → ( 𝐿 ∈ 𝐺 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿 ) ) )
8	7	3ad2ant2	⊢ ( ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) → ( 𝐿 ∈ 𝐺 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿 ) ) )
9	2 8	syl6bi	⊢ ( 𝐺 ∈ Plig → ( 𝐺 ∈ Plig → ( 𝐿 ∈ 𝐺 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿 ) ) ) )
10	9	pm2.43i	⊢ ( 𝐺 ∈ Plig → ( 𝐿 ∈ 𝐺 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿 ) ) )
11	10	imp	⊢ ( ( 𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿 ) )