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\in \mathrm{Plig}\to \neg \varnothing \in G$$

Proof

Step	Hyp	Ref	Expression
1		nsnlplig	$$⊢G\in \mathrm{Plig}\to \neg \left\{\mathrm{V}\right\}\in G$$
2		vprc	$$⊢\neg \mathrm{V}\in \mathrm{V}$$
3		snprc	$$⊢\neg \mathrm{V}\in \mathrm{V}\leftrightarrow \left\{\mathrm{V}\right\}=\varnothing$$
4	2 3	mpbi	$$⊢\left\{\mathrm{V}\right\}=\varnothing$$
5	4	eqcomi	$$⊢\varnothing =\left\{\mathrm{V}\right\}$$
6	5	eleq1i	$$⊢\varnothing \in G\leftrightarrow \left\{\mathrm{V}\right\}\in G$$
7	1 6	sylnibr	$$⊢G\in \mathrm{Plig}\to \neg \varnothing \in G$$