Metamath Proof Explorer

Theorem l2p

Description: For any line in a planar incidence geometry, there exist two different points on the line. (Contributed by AV, 28-Nov-2021)

Ref Expression
Hypothesis l2p.1 ⊢ P = ⋃ G
Assertion l2p ⊢ G ∈ Plig ∧ L ∈ G → ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ L ∧ b ∈ L

Proof

Step Hyp Ref Expression
1 l2p.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 eleq2 ⊢ l = L → a ∈ l ↔ a ∈ L
4 eleq2 ⊢ l = L → b ∈ l ↔ b ∈ L
5 3 4 3anbi23d ⊢ l = L → a ≠ b ∧ a ∈ l ∧ b ∈ l ↔ a ≠ b ∧ a ∈ L ∧ b ∈ L
6 5 2rexbidv ⊢ l = L → ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ l ∧ b ∈ l ↔ ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ L ∧ b ∈ L
7 6 rspccv ⊢ ∀ l ∈ G ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ l ∧ b ∈ l → L ∈ G → ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ L ∧ b ∈ L
8 7 3ad2ant2 ⊢ ∀ 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 → L ∈ G → ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ L ∧ b ∈ L
9 2 8 biimtrdi ⊢ G ∈ Plig → G ∈ Plig → L ∈ G → ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ L ∧ b ∈ L
10 9 pm2.43i ⊢ G ∈ Plig → L ∈ G → ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ L ∧ b ∈ L
11 10 imp ⊢ G ∈ Plig ∧ L ∈ G → ∃ a ∈ P ∃ b ∈ P a ≠ b ∧ a ∈ L ∧ b ∈ L