Theorem clnbgr0vtx

Description: In a null graph (with no vertices), all closed neighborhoods are empty. (Contributed by AV, 15-Nov-2020)

	Ref	Expression
Assertion	clnbgr0vtx	Could not format assertion : No typesetting found for |- ( ( Vtx ` G ) = (/) -> ( G ClNeighbVtx K ) = (/) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nel02	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to \neg K\in \mathrm{Vtx}\left(G\right)$$
2		df-nel	$$⊢K\notin \mathrm{Vtx}\left(G\right)\leftrightarrow \neg K\in \mathrm{Vtx}\left(G\right)$$
3	1 2	sylibr	$$⊢\mathrm{Vtx}\left(G\right)=\varnothing \to K\notin \mathrm{Vtx}\left(G\right)$$
4		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
5	4	clnbgrnvtx0	Could not format ( K e/ ( Vtx ` G ) -> ( G ClNeighbVtx K ) = (/) ) : No typesetting found for |- ( K e/ ( Vtx ` G ) -> ( G ClNeighbVtx K ) = (/) ) with typecode |-
6	3 5	syl	Could not format ( ( Vtx ` G ) = (/) -> ( G ClNeighbVtx K ) = (/) ) : No typesetting found for |- ( ( Vtx ` G ) = (/) -> ( G ClNeighbVtx K ) = (/) ) with typecode |-