# Metamath Proof Explorer

## Theorem uvtx2vtx1edgb

Description: If a hypergraph has two vertices, there is an edge between the vertices iff each vertex is universal. (Contributed by AV, 3-Nov-2020)

Ref Expression
Hypotheses uvtxel.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
isuvtx.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion uvtx2vtx1edgb ${⊢}\left({G}\in \mathrm{UHGraph}\wedge \left|{V}\right|=2\right)\to \left({V}\in {E}↔\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in \mathrm{UnivVtx}\left({G}\right)\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 nbuhgr2vtx1edgb ${⊢}\left({G}\in \mathrm{UHGraph}\wedge \left|{V}\right|=2\right)\to \left({V}\in {E}↔\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)$
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({G}\in \mathrm{UHGraph}\wedge \left|{V}\right|=2\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({G}\in \mathrm{UHGraph}\wedge \left|{V}\right|=2\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 bicomd ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \left|{V}\right|=2\right)\wedge {v}\in {V}\right)\to \left(\forall {n}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\in \left({G}\mathrm{NeighbVtx}{v}\right)↔{v}\in \mathrm{UnivVtx}\left({G}\right)\right)$
8 7 ralbidva ${⊢}\left({G}\in \mathrm{UHGraph}\wedge \left|{V}\right|=2\right)\to \left(\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)↔\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in \mathrm{UnivVtx}\left({G}\right)\right)$
9 3 8 bitrd ${⊢}\left({G}\in \mathrm{UHGraph}\wedge \left|{V}\right|=2\right)\to \left({V}\in {E}↔\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in \mathrm{UnivVtx}\left({G}\right)\right)$