Theorem vtxnbuvtx

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) (Proof shortened by AV, 14-Feb-2022)

	Ref	Expression
Hypothesis	uvtxel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	uvtxel	$$⊢N\in \mathrm{UnivVtx}\left(G\right)\leftrightarrow \left(N\in V\wedge \forall n\in \left(V\setminus \left\{N\right\}\right)n\in \left(G\mathrm{NeighbVtx}N\right)\right)$$
3	2	simprbi	$$⊢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)$$