# Metamath Proof Explorer

## Theorem uspgredg2vtxeu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple pseudograph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 6-Dec-2020)

Ref Expression
Assertion uspgredg2vtxeu ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {E}\in \mathrm{Edg}\left({G}\right)\wedge {Y}\in {E}\right)\to \exists !{y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{E}=\left\{{Y},{y}\right\}$

### Proof

Step Hyp Ref Expression
1 uspgrupgr ${⊢}{G}\in \mathrm{USHGraph}\to {G}\in \mathrm{UPGraph}$
2 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
3 eqid ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{Edg}\left({G}\right)$
4 2 3 upgredg2vtx ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {E}\in \mathrm{Edg}\left({G}\right)\wedge {Y}\in {E}\right)\to \exists {y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{E}=\left\{{Y},{y}\right\}$
5 1 4 syl3an1 ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {E}\in \mathrm{Edg}\left({G}\right)\wedge {Y}\in {E}\right)\to \exists {y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{E}=\left\{{Y},{y}\right\}$
6 eqtr2 ${⊢}\left({E}=\left\{{Y},{y}\right\}\wedge {E}=\left\{{Y},{x}\right\}\right)\to \left\{{Y},{y}\right\}=\left\{{Y},{x}\right\}$
7 vex ${⊢}{y}\in \mathrm{V}$
8 vex ${⊢}{x}\in \mathrm{V}$
9 7 8 preqr2 ${⊢}\left\{{Y},{y}\right\}=\left\{{Y},{x}\right\}\to {y}={x}$
10 6 9 syl ${⊢}\left({E}=\left\{{Y},{y}\right\}\wedge {E}=\left\{{Y},{x}\right\}\right)\to {y}={x}$
11 10 a1i ${⊢}\left(\left({G}\in \mathrm{USHGraph}\wedge {E}\in \mathrm{Edg}\left({G}\right)\wedge {Y}\in {E}\right)\wedge \left({y}\in \mathrm{Vtx}\left({G}\right)\wedge {x}\in \mathrm{Vtx}\left({G}\right)\right)\right)\to \left(\left({E}=\left\{{Y},{y}\right\}\wedge {E}=\left\{{Y},{x}\right\}\right)\to {y}={x}\right)$
12 11 ralrimivva ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {E}\in \mathrm{Edg}\left({G}\right)\wedge {Y}\in {E}\right)\to \forall {y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left(\left({E}=\left\{{Y},{y}\right\}\wedge {E}=\left\{{Y},{x}\right\}\right)\to {y}={x}\right)$
13 preq2 ${⊢}{y}={x}\to \left\{{Y},{y}\right\}=\left\{{Y},{x}\right\}$
14 13 eqeq2d ${⊢}{y}={x}\to \left({E}=\left\{{Y},{y}\right\}↔{E}=\left\{{Y},{x}\right\}\right)$
15 14 reu4 ${⊢}\exists !{y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{E}=\left\{{Y},{y}\right\}↔\left(\exists {y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{E}=\left\{{Y},{y}\right\}\wedge \forall {y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left(\left({E}=\left\{{Y},{y}\right\}\wedge {E}=\left\{{Y},{x}\right\}\right)\to {y}={x}\right)\right)$
16 5 12 15 sylanbrc ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {E}\in \mathrm{Edg}\left({G}\right)\wedge {Y}\in {E}\right)\to \exists !{y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{E}=\left\{{Y},{y}\right\}$