# Metamath Proof Explorer

## Theorem umgr2edg

Description: If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised 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 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)$

### Proof

Step Hyp Ref Expression
1 usgrf1oedg.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
2 usgrf1oedg.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 umgruhgr ${⊢}{G}\in \mathrm{UMGraph}\to {G}\in \mathrm{UHGraph}$
4 3 anim1i ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {A}\ne {B}\right)\to \left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)$
5 4 adantr ${⊢}\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 \left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)$
6 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
7 6 2 umgrpredgv ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{N},{A}\right\}\in {E}\right)\to \left({N}\in \mathrm{Vtx}\left({G}\right)\wedge {A}\in \mathrm{Vtx}\left({G}\right)\right)$
8 7 ad2ant2r ${⊢}\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 \left({N}\in \mathrm{Vtx}\left({G}\right)\wedge {A}\in \mathrm{Vtx}\left({G}\right)\right)$
9 8 simprd ${⊢}\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 {A}\in \mathrm{Vtx}\left({G}\right)$
10 6 2 umgrpredgv ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{B},{N}\right\}\in {E}\right)\to \left({B}\in \mathrm{Vtx}\left({G}\right)\wedge {N}\in \mathrm{Vtx}\left({G}\right)\right)$
11 10 ad2ant2rl ${⊢}\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 \left({B}\in \mathrm{Vtx}\left({G}\right)\wedge {N}\in \mathrm{Vtx}\left({G}\right)\right)$
12 11 simpld ${⊢}\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 {B}\in \mathrm{Vtx}\left({G}\right)$
13 8 simpld ${⊢}\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 {N}\in \mathrm{Vtx}\left({G}\right)$
14 simpr ${⊢}\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 \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)$
15 1 2 6 uhgr2edg ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Vtx}\left({G}\right)\wedge {N}\in \mathrm{Vtx}\left({G}\right)\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)$
16 5 9 12 13 14 15 syl131anc ${⊢}\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)$