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	⊢ ( 𝐺 ∈ Plig → ¬ ∅ ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		nsnlplig	⊢ ( 𝐺 ∈ Plig → ¬ { V } ∈ 𝐺 )
2		vprc	⊢ ¬ V ∈ V
3		snprc	⊢ ( ¬ V ∈ V ↔ { V } = ∅ )
4	2 3	mpbi	⊢ { V } = ∅
5	4	eqcomi	⊢ ∅ = { V }
6	5	eleq1i	⊢ ( ∅ ∈ 𝐺 ↔ { V } ∈ 𝐺 )
7	1 6	sylnibr	⊢ ( 𝐺 ∈ Plig → ¬ ∅ ∈ 𝐺 )