Metamath Proof Explorer

Theorem n0lplig

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

Ref Expression
Assertion n0lplig 
|- ( G e. Plig -> -. (/) e. G )

Proof

Step Hyp Ref Expression
1 nsnlplig 
 |-  ( G e. Plig -> -. { _V } e. G )
2 vprc 
 |-  -. _V e. _V
3 snprc 
 |-  ( -. _V e. _V <-> { _V } = (/) )
4 2 3 mpbi 
 |-  { _V } = (/)
5 4 eqcomi 
 |-  (/) = { _V }
6 5 eleq1i 
 |-  ( (/) e. G <-> { _V } e. G )
7 1 6 sylnibr 
 |-  ( G e. Plig -> -. (/) e. G )