Theorem clnbgr0edg

Description: In an empty graph (with no edges), all closed neighborhoods consists of a single vertex. (Contributed by AV, 10-May-2025)

	Ref	Expression
Assertion	clnbgr0edg	Could not format assertion : No typesetting found for |- ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( G ClNeighbVtx K ) = { K } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
2	1	dfclnbgr4	Could not format ( K e. ( Vtx ` G ) -> ( G ClNeighbVtx K ) = ( { K } u. ( G NeighbVtx K ) ) ) : No typesetting found for |- ( K e. ( Vtx ` G ) -> ( G ClNeighbVtx K ) = ( { K } u. ( G NeighbVtx K ) ) ) with typecode |-
3	2	adantl	Could not format ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( G ClNeighbVtx K ) = ( { K } u. ( G NeighbVtx K ) ) ) : No typesetting found for |- ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( G ClNeighbVtx K ) = ( { K } u. ( G NeighbVtx K ) ) ) with typecode |-
4		nbgr0edg	$$⊢\mathrm{Edg}\left(G\right)=\varnothing \to G\mathrm{NeighbVtx}K=\varnothing$$
5	4	adantr	$$⊢\left(\mathrm{Edg}\left(G\right)=\varnothing \wedge K\in \mathrm{Vtx}\left(G\right)\right)\to G\mathrm{NeighbVtx}K=\varnothing$$
6	5	uneq2d	$$⊢\left(\mathrm{Edg}\left(G\right)=\varnothing \wedge K\in \mathrm{Vtx}\left(G\right)\right)\to \left\{K\right\}\cup \left(G\mathrm{NeighbVtx}K\right)=\left\{K\right\}\cup \varnothing$$
7		un0	$$⊢\left\{K\right\}\cup \varnothing =\left\{K\right\}$$
8	7	a1i	$$⊢\left(\mathrm{Edg}\left(G\right)=\varnothing \wedge K\in \mathrm{Vtx}\left(G\right)\right)\to \left\{K\right\}\cup \varnothing =\left\{K\right\}$$
9	3 6 8	3eqtrd	Could not format ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( G ClNeighbVtx K ) = { K } ) : No typesetting found for |- ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( G ClNeighbVtx K ) = { K } ) with typecode |-