Theorem eulplig

Description: Through two distinct points of a planar incidence geometry, there is a unique line. (Contributed by BJ, 2-Dec-2021)

	Ref	Expression
Hypothesis	eulplig.1	⊢ 𝑃 = ∪ 𝐺
Assertion	eulplig	⊢ ( ( 𝐺 ∈ Plig ∧ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ) → ∃! 𝑙 ∈ 𝐺 ( 𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙 ) )

Proof

Step	Hyp	Ref	Expression
1		eulplig.1	⊢ 𝑃 = ∪ 𝐺
2	1	isplig	⊢ ( 𝐺 ∈ Plig → ( 𝐺 ∈ Plig ↔ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) ) )
3	2	ibi	⊢ ( 𝐺 ∈ Plig → ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) )
4		simp1	⊢ ( ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) → ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) )
5		simpl	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → 𝑎 = 𝐴 )
6		simpr	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
7	5 6	neeq12d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ≠ 𝑏 ↔ 𝐴 ≠ 𝐵 ) )
8		eleq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ∈ 𝑙 ↔ 𝐴 ∈ 𝑙 ) )
9		eleq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∈ 𝑙 ↔ 𝐵 ∈ 𝑙 ) )
10	8 9	bi2anan9	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ↔ ( 𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙 ) ) )
11	10	reubidv	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ↔ ∃! 𝑙 ∈ 𝐺 ( 𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙 ) ) )
12	7 11	imbi12d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ↔ ( 𝐴 ≠ 𝐵 → ∃! 𝑙 ∈ 𝐺 ( 𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙 ) ) ) )
13	12	rspc2gv	⊢ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) → ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) → ( 𝐴 ≠ 𝐵 → ∃! 𝑙 ∈ 𝐺 ( 𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙 ) ) ) )
14	13	com23	⊢ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) → ( 𝐴 ≠ 𝐵 → ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) → ∃! 𝑙 ∈ 𝐺 ( 𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙 ) ) ) )
15	14	imp	⊢ ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) → ∃! 𝑙 ∈ 𝐺 ( 𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙 ) ) )
16	15	com12	⊢ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) → ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑙 ∈ 𝐺 ( 𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙 ) ) )
17	3 4 16	3syl	⊢ ( 𝐺 ∈ Plig → ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑙 ∈ 𝐺 ( 𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙 ) ) )
18	17	imp	⊢ ( ( 𝐺 ∈ Plig ∧ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ 𝐴 ≠ 𝐵 ) ) → ∃! 𝑙 ∈ 𝐺 ( 𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙 ) )