# Metamath Proof Explorer

## Theorem nbusgredgeu0

Description: For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 27-Oct-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nbusgrf1o1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
nbusgrf1o1.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
nbusgrf1o1.n ${⊢}{N}={G}\mathrm{NeighbVtx}{U}$
nbusgrf1o1.i ${⊢}{I}=\left\{{e}\in {E}|{U}\in {e}\right\}$
Assertion nbusgredgeu0 ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \exists !{i}\in {I}\phantom{\rule{.4em}{0ex}}{i}=\left\{{U},{M}\right\}$

### Proof

Step Hyp Ref Expression
1 nbusgrf1o1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 nbusgrf1o1.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 nbusgrf1o1.n ${⊢}{N}={G}\mathrm{NeighbVtx}{U}$
4 nbusgrf1o1.i ${⊢}{I}=\left\{{e}\in {E}|{U}\in {e}\right\}$
5 simpll ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to {G}\in \mathrm{USGraph}$
6 3 eleq2i ${⊢}{M}\in {N}↔{M}\in \left({G}\mathrm{NeighbVtx}{U}\right)$
7 nbgrsym ${⊢}{M}\in \left({G}\mathrm{NeighbVtx}{U}\right)↔{U}\in \left({G}\mathrm{NeighbVtx}{M}\right)$
8 7 a1i ${⊢}\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\to \left({M}\in \left({G}\mathrm{NeighbVtx}{U}\right)↔{U}\in \left({G}\mathrm{NeighbVtx}{M}\right)\right)$
9 8 biimpd ${⊢}\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\to \left({M}\in \left({G}\mathrm{NeighbVtx}{U}\right)\to {U}\in \left({G}\mathrm{NeighbVtx}{M}\right)\right)$
10 6 9 syl5bi ${⊢}\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\to \left({M}\in {N}\to {U}\in \left({G}\mathrm{NeighbVtx}{M}\right)\right)$
11 10 imp ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to {U}\in \left({G}\mathrm{NeighbVtx}{M}\right)$
12 2 nbusgredgeu ${⊢}\left({G}\in \mathrm{USGraph}\wedge {U}\in \left({G}\mathrm{NeighbVtx}{M}\right)\right)\to \exists !{i}\in {E}\phantom{\rule{.4em}{0ex}}{i}=\left\{{U},{M}\right\}$
13 5 11 12 syl2anc ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \exists !{i}\in {E}\phantom{\rule{.4em}{0ex}}{i}=\left\{{U},{M}\right\}$
14 df-reu ${⊢}\exists !{i}\in {E}\phantom{\rule{.4em}{0ex}}{i}=\left\{{U},{M}\right\}↔\exists !{i}\phantom{\rule{.4em}{0ex}}\left({i}\in {E}\wedge {i}=\left\{{U},{M}\right\}\right)$
15 13 14 sylib ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \exists !{i}\phantom{\rule{.4em}{0ex}}\left({i}\in {E}\wedge {i}=\left\{{U},{M}\right\}\right)$
16 anass ${⊢}\left(\left({i}\in {E}\wedge {U}\in {i}\right)\wedge {i}=\left\{{U},{M}\right\}\right)↔\left({i}\in {E}\wedge \left({U}\in {i}\wedge {i}=\left\{{U},{M}\right\}\right)\right)$
17 prid1g ${⊢}{U}\in {V}\to {U}\in \left\{{U},{M}\right\}$
18 17 ad2antlr ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to {U}\in \left\{{U},{M}\right\}$
19 eleq2 ${⊢}{i}=\left\{{U},{M}\right\}\to \left({U}\in {i}↔{U}\in \left\{{U},{M}\right\}\right)$
20 18 19 syl5ibrcom ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \left({i}=\left\{{U},{M}\right\}\to {U}\in {i}\right)$
21 20 pm4.71rd ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \left({i}=\left\{{U},{M}\right\}↔\left({U}\in {i}\wedge {i}=\left\{{U},{M}\right\}\right)\right)$
22 21 bicomd ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \left(\left({U}\in {i}\wedge {i}=\left\{{U},{M}\right\}\right)↔{i}=\left\{{U},{M}\right\}\right)$
23 22 anbi2d ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \left(\left({i}\in {E}\wedge \left({U}\in {i}\wedge {i}=\left\{{U},{M}\right\}\right)\right)↔\left({i}\in {E}\wedge {i}=\left\{{U},{M}\right\}\right)\right)$
24 16 23 syl5bb ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \left(\left(\left({i}\in {E}\wedge {U}\in {i}\right)\wedge {i}=\left\{{U},{M}\right\}\right)↔\left({i}\in {E}\wedge {i}=\left\{{U},{M}\right\}\right)\right)$
25 24 eubidv ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \left(\exists !{i}\phantom{\rule{.4em}{0ex}}\left(\left({i}\in {E}\wedge {U}\in {i}\right)\wedge {i}=\left\{{U},{M}\right\}\right)↔\exists !{i}\phantom{\rule{.4em}{0ex}}\left({i}\in {E}\wedge {i}=\left\{{U},{M}\right\}\right)\right)$
26 15 25 mpbird ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \exists !{i}\phantom{\rule{.4em}{0ex}}\left(\left({i}\in {E}\wedge {U}\in {i}\right)\wedge {i}=\left\{{U},{M}\right\}\right)$
27 df-reu ${⊢}\exists !{i}\in {I}\phantom{\rule{.4em}{0ex}}{i}=\left\{{U},{M}\right\}↔\exists !{i}\phantom{\rule{.4em}{0ex}}\left({i}\in {I}\wedge {i}=\left\{{U},{M}\right\}\right)$
28 eleq2 ${⊢}{e}={i}\to \left({U}\in {e}↔{U}\in {i}\right)$
29 28 4 elrab2 ${⊢}{i}\in {I}↔\left({i}\in {E}\wedge {U}\in {i}\right)$
30 29 anbi1i ${⊢}\left({i}\in {I}\wedge {i}=\left\{{U},{M}\right\}\right)↔\left(\left({i}\in {E}\wedge {U}\in {i}\right)\wedge {i}=\left\{{U},{M}\right\}\right)$
31 30 eubii ${⊢}\exists !{i}\phantom{\rule{.4em}{0ex}}\left({i}\in {I}\wedge {i}=\left\{{U},{M}\right\}\right)↔\exists !{i}\phantom{\rule{.4em}{0ex}}\left(\left({i}\in {E}\wedge {U}\in {i}\right)\wedge {i}=\left\{{U},{M}\right\}\right)$
32 27 31 bitri ${⊢}\exists !{i}\in {I}\phantom{\rule{.4em}{0ex}}{i}=\left\{{U},{M}\right\}↔\exists !{i}\phantom{\rule{.4em}{0ex}}\left(\left({i}\in {E}\wedge {U}\in {i}\right)\wedge {i}=\left\{{U},{M}\right\}\right)$
33 26 32 sylibr ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {U}\in {V}\right)\wedge {M}\in {N}\right)\to \exists !{i}\in {I}\phantom{\rule{.4em}{0ex}}{i}=\left\{{U},{M}\right\}$