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 
|- ( G e. Plig -> -. { A } e. G )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. G = U. G
2 1 l2p 
 |-  ( ( G e. Plig /\ { A } e. G ) -> E. a e. U. G E. b e. U. G ( a =/= b /\ a e. { A } /\ b e. { A } ) )
3 elsni 
 |-  ( a e. { A } -> a = A )
4 elsni 
 |-  ( b e. { A } -> b = A )
5 eqtr3 
 |-  ( ( a = A /\ b = A ) -> a = b )
6 eqneqall 
 |-  ( a = b -> ( a =/= b -> -. { A } e. G ) )
7 5 6 syl 
 |-  ( ( a = A /\ b = A ) -> ( a =/= b -> -. { A } e. G ) )
8 3 4 7 syl2an 
 |-  ( ( a e. { A } /\ b e. { A } ) -> ( a =/= b -> -. { A } e. G ) )
9 8 impcom 
 |-  ( ( a =/= b /\ ( a e. { A } /\ b e. { A } ) ) -> -. { A } e. G )
10 9 3impb 
 |-  ( ( a =/= b /\ a e. { A } /\ b e. { A } ) -> -. { A } e. G )
11 10 a1i 
 |-  ( ( a e. U. G /\ b e. U. G ) -> ( ( a =/= b /\ a e. { A } /\ b e. { A } ) -> -. { A } e. G ) )
12 11 rexlimivv 
 |-  ( E. a e. U. G E. b e. U. G ( a =/= b /\ a e. { A } /\ b e. { A } ) -> -. { A } e. G )
13 2 12 syl 
 |-  ( ( G e. Plig /\ { A } e. G ) -> -. { A } e. G )
14 13 pm2.01da 
 |-  ( G e. Plig -> -. { A } e. G )