# 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}=\bigcup {G}$
Assertion eulplig ${⊢}\left({G}\in \mathrm{Plig}\wedge \left(\left({A}\in {P}\wedge {B}\in {P}\right)\wedge {A}\ne {B}\right)\right)\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({A}\in {l}\wedge {B}\in {l}\right)$

### Proof

Step Hyp Ref Expression
1 eulplig.1 ${⊢}{P}=\bigcup {G}$
2 1 isplig ${⊢}{G}\in \mathrm{Plig}\to \left({G}\in \mathrm{Plig}↔\left(\forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {G}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)\right)$
3 2 ibi ${⊢}{G}\in \mathrm{Plig}\to \left(\forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {G}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)$
4 simp1 ${⊢}\left(\forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {G}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\forall {l}\in {G}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)\to \forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)$
5 simpl ${⊢}\left({a}={A}\wedge {b}={B}\right)\to {a}={A}$
6 simpr ${⊢}\left({a}={A}\wedge {b}={B}\right)\to {b}={B}$
7 5 6 neeq12d ${⊢}\left({a}={A}\wedge {b}={B}\right)\to \left({a}\ne {b}↔{A}\ne {B}\right)$
8 eleq1 ${⊢}{a}={A}\to \left({a}\in {l}↔{A}\in {l}\right)$
9 eleq1 ${⊢}{b}={B}\to \left({b}\in {l}↔{B}\in {l}\right)$
10 8 9 bi2anan9 ${⊢}\left({a}={A}\wedge {b}={B}\right)\to \left(\left({a}\in {l}\wedge {b}\in {l}\right)↔\left({A}\in {l}\wedge {B}\in {l}\right)\right)$
11 10 reubidv ${⊢}\left({a}={A}\wedge {b}={B}\right)\to \left(\exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)↔\exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({A}\in {l}\wedge {B}\in {l}\right)\right)$
12 7 11 imbi12d ${⊢}\left({a}={A}\wedge {b}={B}\right)\to \left(\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)↔\left({A}\ne {B}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({A}\in {l}\wedge {B}\in {l}\right)\right)\right)$
13 12 rspc2gv ${⊢}\left({A}\in {P}\wedge {B}\in {P}\right)\to \left(\forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\to \left({A}\ne {B}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({A}\in {l}\wedge {B}\in {l}\right)\right)\right)$
14 13 com23 ${⊢}\left({A}\in {P}\wedge {B}\in {P}\right)\to \left({A}\ne {B}\to \left(\forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({A}\in {l}\wedge {B}\in {l}\right)\right)\right)$
15 14 imp ${⊢}\left(\left({A}\in {P}\wedge {B}\in {P}\right)\wedge {A}\ne {B}\right)\to \left(\forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({A}\in {l}\wedge {B}\in {l}\right)\right)$
16 15 com12 ${⊢}\forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {b}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\to \left(\left(\left({A}\in {P}\wedge {B}\in {P}\right)\wedge {A}\ne {B}\right)\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({A}\in {l}\wedge {B}\in {l}\right)\right)$
17 3 4 16 3syl ${⊢}{G}\in \mathrm{Plig}\to \left(\left(\left({A}\in {P}\wedge {B}\in {P}\right)\wedge {A}\ne {B}\right)\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({A}\in {l}\wedge {B}\in {l}\right)\right)$
18 17 imp ${⊢}\left({G}\in \mathrm{Plig}\wedge \left(\left({A}\in {P}\wedge {B}\in {P}\right)\wedge {A}\ne {B}\right)\right)\to \exists !{l}\in {G}\phantom{\rule{.4em}{0ex}}\left({A}\in {l}\wedge {B}\in {l}\right)$