Metamath Proof Explorer

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 ⊢P=⋃G
Assertion eulplig ⊢G∈Plig∧A∈P∧B∈P∧A≠B→∃!l∈GA∈l∧B∈l

Proof

Step Hyp Ref Expression
1 eulplig.1 ⊢P=⋃G
2 1 isplig ⊢G∈Plig→G∈Plig↔∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l∧∀l∈G∃a∈P∃b∈Pa≠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∈Pa≠b→∃!l∈Ga∈l∧b∈l∧∀l∈G∃a∈P∃b∈Pa≠b∧a∈l∧b∈l∧∃a∈P∃b∈P∃c∈P∀l∈G¬a∈l∧b∈l∧c∈l
4 simp1 ⊢∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l∧∀l∈G∃a∈P∃b∈Pa≠b∧a∈l∧b∈l∧∃a∈P∃b∈P∃c∈P∀l∈G¬a∈l∧b∈l∧c∈l→∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l
5 simpl ⊢a=A∧b=B→a=A
6 simpr ⊢a=A∧b=B→b=B
7 5 6 neeq12d ⊢a=A∧b=B→a≠b↔A≠B
8 eleq1 ⊢a=A→a∈l↔A∈l
9 eleq1 ⊢b=B→b∈l↔B∈l
10 8 9 bi2anan9 ⊢a=A∧b=B→a∈l∧b∈l↔A∈l∧B∈l
11 10 reubidv ⊢a=A∧b=B→∃!l∈Ga∈l∧b∈l↔∃!l∈GA∈l∧B∈l
12 7 11 imbi12d ⊢a=A∧b=B→a≠b→∃!l∈Ga∈l∧b∈l↔A≠B→∃!l∈GA∈l∧B∈l
13 12 rspc2gv ⊢A∈P∧B∈P→∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l→A≠B→∃!l∈GA∈l∧B∈l
14 13 com23 ⊢A∈P∧B∈P→A≠B→∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l→∃!l∈GA∈l∧B∈l
15 14 imp ⊢A∈P∧B∈P∧A≠B→∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l→∃!l∈GA∈l∧B∈l
16 15 com12 ⊢∀a∈P∀b∈Pa≠b→∃!l∈Ga∈l∧b∈l→A∈P∧B∈P∧A≠B→∃!l∈GA∈l∧B∈l
17 3 4 16 3syl ⊢G∈Plig→A∈P∧B∈P∧A≠B→∃!l∈GA∈l∧B∈l
18 17 imp ⊢G∈Plig∧A∈P∧B∈P∧A≠B→∃!l∈GA∈l∧B∈l