# Metamath Proof Explorer

## Theorem uvtx2vtx1edg

Description: If a graph has two vertices, and there is an edge between the vertices, then each vertex is universal. (Contributed by AV, 1-Nov-2020) (Revised by AV, 25-Mar-2021) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypotheses uvtxel.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
isuvtx.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion uvtx2vtx1edg ${⊢}\left(\left|{V}\right|=2\wedge {V}\in {E}\right)\to \forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in \mathrm{UnivVtx}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 uvtxel.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 isuvtx.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 1 2 nbgr2vtx1edg ${⊢}\left(\left|{V}\right|=2\wedge {V}\in {E}\right)\to \forall {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)$
4 1 uvtxel ${⊢}{v}\in \mathrm{UnivVtx}\left({G}\right)↔\left({v}\in {V}\wedge \forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right)$
5 4 a1i ${⊢}\left(\left|{V}\right|=2\wedge {V}\in {E}\right)\to \left({v}\in \mathrm{UnivVtx}\left({G}\right)↔\left({v}\in {V}\wedge \forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right)\right)$
6 5 baibd ${⊢}\left(\left(\left|{V}\right|=2\wedge {V}\in {E}\right)\wedge {v}\in {V}\right)\to \left({v}\in \mathrm{UnivVtx}\left({G}\right)↔\forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right)$
7 6 ralbidva ${⊢}\left(\left|{V}\right|=2\wedge {V}\in {E}\right)\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in \mathrm{UnivVtx}\left({G}\right)↔\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)\right)$
8 3 7 mpbird ${⊢}\left(\left|{V}\right|=2\wedge {V}\in {E}\right)\to \forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in \mathrm{UnivVtx}\left({G}\right)$