Theorem uvtxnbgrss

Description: A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 30-Oct-2020)

	Ref	Expression
Hypothesis	uvtxel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	uvtxnbgrss	$$⊢N\in \mathrm{UnivVtx}\left(G\right)\to V\setminus \left\{N\right\}\subseteq G\mathrm{NeighbVtx}N$$

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	vtxnbuvtx	$$⊢N\in \mathrm{UnivVtx}\left(G\right)\to \forall n\in \left(V\setminus \left\{N\right\}\right)n\in \left(G\mathrm{NeighbVtx}N\right)$$
3		dfss3	$$⊢V\setminus \left\{N\right\}\subseteq G\mathrm{NeighbVtx}N\leftrightarrow \forall n\in \left(V\setminus \left\{N\right\}\right)n\in \left(G\mathrm{NeighbVtx}N\right)$$
4	2 3	sylibr	$$⊢N\in \mathrm{UnivVtx}\left(G\right)\to V\setminus \left\{N\right\}\subseteq G\mathrm{NeighbVtx}N$$