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 syl6bi 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