Metamath Proof Explorer


Theorem nsnlplig

Description: There is no "one-point line" in a planar incidence geometry. (Contributed by BJ, 2-Dec-2021) (Proof shortened by AV, 5-Dec-2021)

Ref Expression
Assertion nsnlplig GPlig¬AG

Proof

Step Hyp Ref Expression
1 eqid G=G
2 1 l2p GPligAGaGbGabaAbA
3 elsni aAa=A
4 elsni bAb=A
5 eqtr3 a=Ab=Aa=b
6 eqneqall a=bab¬AG
7 5 6 syl a=Ab=Aab¬AG
8 3 4 7 syl2an aAbAab¬AG
9 8 impcom abaAbA¬AG
10 9 3impb abaAbA¬AG
11 10 a1i aGbGabaAbA¬AG
12 11 rexlimivv aGbGabaAbA¬AG
13 2 12 syl GPligAG¬AG
14 13 pm2.01da GPlig¬AG