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 ∈ G A ∈ l ∧ B ∈ l

Proof

Step Hyp Ref Expression
1 eulplig.1 ⊢ P = ⋃ G
2 1 isplig ⊢ G ∈ Plig → G ∈ Plig ↔ ∀ a ∈ P ∀ b ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l ∧ ∀ l ∈ G ∃ a ∈ P ∃ b ∈ P a ≠ 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 ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l ∧ ∀ l ∈ G ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ l ∧ b ∈ l ∧ ∃ a ∈ P ∃ b ∈ P ∃ c ∈ P ∀ l ∈ G ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l
4 simp1 ⊢ ∀ a ∈ P ∀ b ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l ∧ ∀ l ∈ G ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ l ∧ b ∈ l ∧ ∃ a ∈ P ∃ b ∈ P ∃ c ∈ P ∀ l ∈ G ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l → ∀ a ∈ P ∀ b ∈ P a ≠ b → ∃! l ∈ G a ∈ 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 ∈ G a ∈ l ∧ b ∈ l ↔ ∃! l ∈ G A ∈ l ∧ B ∈ l
12 7 11 imbi12d ⊢ a = A ∧ b = B → a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l ↔ A ≠ B → ∃! l ∈ G A ∈ l ∧ B ∈ l
13 12 rspc2gv ⊢ A ∈ P ∧ B ∈ P → ∀ a ∈ P ∀ b ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l → A ≠ B → ∃! l ∈ G A ∈ l ∧ B ∈ l
14 13 com23 ⊢ A ∈ P ∧ B ∈ P → A ≠ B → ∀ a ∈ P ∀ b ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l → ∃! l ∈ G A ∈ l ∧ B ∈ l
15 14 imp ⊢ A ∈ P ∧ B ∈ P ∧ A ≠ B → ∀ a ∈ P ∀ b ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l → ∃! l ∈ G A ∈ l ∧ B ∈ l
16 15 com12 ⊢ ∀ a ∈ P ∀ b ∈ P a ≠ b → ∃! l ∈ G a ∈ l ∧ b ∈ l → A ∈ P ∧ B ∈ P ∧ A ≠ B → ∃! l ∈ G A ∈ l ∧ B ∈ l
17 3 4 16 3syl ⊢ G ∈ Plig → A ∈ P ∧ B ∈ P ∧ A ≠ B → ∃! l ∈ G A ∈ l ∧ B ∈ l
18 17 imp ⊢ G ∈ Plig ∧ A ∈ P ∧ B ∈ P ∧ A ≠ B → ∃! l ∈ G A ∈ l ∧ B ∈ l