Theorem eulplig 28847

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

Hypothesis

Ref	Expression
eulplig.1	⊢ 𝑃 = ∪ 𝐺

Assertion

Ref	Expression
eulplig	⊢ ((𝐺 ∈ Plig ∧ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ 𝐴 ≠ 𝐵)) → ∃!𝑙 ∈ 𝐺 (𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙))

Distinct variable groups:   𝐺,𝑙   𝐴,𝑙   𝐵,𝑙

Allowed substitution hint:   𝑃(𝑙)

Proof of Theorem eulplig

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  ∃!wreu 3066  ∪ cuni 4839  Pligcplig 28836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1542  df-ex 1783  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-plig 28837

This theorem is referenced by: (None)