# Metamath Proof Explorer

## Theorem usgr2edg

Description: If a vertex is adjacent to two different vertices in a simple graph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 17-Oct-2020) (Proof shortened by AV, 11-Feb-2021)

Ref Expression
Hypotheses usgrf1oedg.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
usgrf1oedg.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion usgr2edg ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {A}\ne {B}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to \exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 usgrf1oedg.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
2 usgrf1oedg.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 usgrumgr ${⊢}{G}\in \mathrm{USGraph}\to {G}\in \mathrm{UMGraph}$
4 1 2 umgr2edg ${⊢}\left(\left({G}\in \mathrm{UMGraph}\wedge {A}\ne {B}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to \exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)$
5 3 4 sylanl1 ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {A}\ne {B}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to \exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)$