# Metamath Proof Explorer

## Theorem usgredg4

Description: For a vertex incident to an edge there is another vertex incident to the edge. (Contributed by Alexander van der Vekens, 18-Dec-2017) (Revised by AV, 17-Oct-2020)

Ref Expression
Hypotheses usgredg3.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
usgredg3.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
Assertion usgredg4 ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\wedge {Y}\in {E}\left({X}\right)\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}$

### Proof

Step Hyp Ref Expression
1 usgredg3.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 usgredg3.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 1 2 usgredg3 ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}\left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)$
4 eleq2 ${⊢}{E}\left({X}\right)=\left\{{x},{z}\right\}\to \left({Y}\in {E}\left({X}\right)↔{Y}\in \left\{{x},{z}\right\}\right)$
5 4 adantl ${⊢}\left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\to \left({Y}\in {E}\left({X}\right)↔{Y}\in \left\{{x},{z}\right\}\right)$
6 5 adantl ${⊢}\left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\to \left({Y}\in {E}\left({X}\right)↔{Y}\in \left\{{x},{z}\right\}\right)$
7 simplrr ${⊢}\left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\to {z}\in {V}$
8 7 adantl ${⊢}\left({Y}={x}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to {z}\in {V}$
9 preq2 ${⊢}{y}={z}\to \left\{{x},{y}\right\}=\left\{{x},{z}\right\}$
10 9 eqeq2d ${⊢}{y}={z}\to \left(\left\{{x},{z}\right\}=\left\{{x},{y}\right\}↔\left\{{x},{z}\right\}=\left\{{x},{z}\right\}\right)$
11 10 adantl ${⊢}\left(\left({Y}={x}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\wedge {y}={z}\right)\to \left(\left\{{x},{z}\right\}=\left\{{x},{y}\right\}↔\left\{{x},{z}\right\}=\left\{{x},{z}\right\}\right)$
12 eqidd ${⊢}\left({Y}={x}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to \left\{{x},{z}\right\}=\left\{{x},{z}\right\}$
13 8 11 12 rspcedvd ${⊢}\left({Y}={x}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left\{{x},{z}\right\}=\left\{{x},{y}\right\}$
14 simprr ${⊢}\left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\to {E}\left({X}\right)=\left\{{x},{z}\right\}$
15 preq1 ${⊢}{Y}={x}\to \left\{{Y},{y}\right\}=\left\{{x},{y}\right\}$
16 14 15 eqeqan12rd ${⊢}\left({Y}={x}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to \left({E}\left({X}\right)=\left\{{Y},{y}\right\}↔\left\{{x},{z}\right\}=\left\{{x},{y}\right\}\right)$
17 16 rexbidv ${⊢}\left({Y}={x}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to \left(\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}↔\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left\{{x},{z}\right\}=\left\{{x},{y}\right\}\right)$
18 13 17 mpbird ${⊢}\left({Y}={x}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}$
19 18 ex ${⊢}{Y}={x}\to \left(\left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}\right)$
20 simplrl ${⊢}\left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\to {x}\in {V}$
21 20 adantl ${⊢}\left({Y}={z}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to {x}\in {V}$
22 preq2 ${⊢}{y}={x}\to \left\{{z},{y}\right\}=\left\{{z},{x}\right\}$
23 22 eqeq2d ${⊢}{y}={x}\to \left(\left\{{x},{z}\right\}=\left\{{z},{y}\right\}↔\left\{{x},{z}\right\}=\left\{{z},{x}\right\}\right)$
24 23 adantl ${⊢}\left(\left({Y}={z}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\wedge {y}={x}\right)\to \left(\left\{{x},{z}\right\}=\left\{{z},{y}\right\}↔\left\{{x},{z}\right\}=\left\{{z},{x}\right\}\right)$
25 prcom ${⊢}\left\{{x},{z}\right\}=\left\{{z},{x}\right\}$
26 25 a1i ${⊢}\left({Y}={z}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to \left\{{x},{z}\right\}=\left\{{z},{x}\right\}$
27 21 24 26 rspcedvd ${⊢}\left({Y}={z}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left\{{x},{z}\right\}=\left\{{z},{y}\right\}$
28 preq1 ${⊢}{Y}={z}\to \left\{{Y},{y}\right\}=\left\{{z},{y}\right\}$
29 14 28 eqeqan12rd ${⊢}\left({Y}={z}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to \left({E}\left({X}\right)=\left\{{Y},{y}\right\}↔\left\{{x},{z}\right\}=\left\{{z},{y}\right\}\right)$
30 29 rexbidv ${⊢}\left({Y}={z}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to \left(\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}↔\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left\{{x},{z}\right\}=\left\{{z},{y}\right\}\right)$
31 27 30 mpbird ${⊢}\left({Y}={z}\wedge \left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}$
32 31 ex ${⊢}{Y}={z}\to \left(\left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}\right)$
33 19 32 jaoi ${⊢}\left({Y}={x}\vee {Y}={z}\right)\to \left(\left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}\right)$
34 elpri ${⊢}{Y}\in \left\{{x},{z}\right\}\to \left({Y}={x}\vee {Y}={z}\right)$
35 33 34 syl11 ${⊢}\left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\to \left({Y}\in \left\{{x},{z}\right\}\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}\right)$
36 6 35 sylbid ${⊢}\left(\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\right)\to \left({Y}\in {E}\left({X}\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}\right)$
37 36 ex ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\wedge \left({x}\in {V}\wedge {z}\in {V}\right)\right)\to \left(\left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\to \left({Y}\in {E}\left({X}\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}\right)\right)$
38 37 rexlimdvva ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\to \left(\exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}\left({x}\ne {z}\wedge {E}\left({X}\right)=\left\{{x},{z}\right\}\right)\to \left({Y}\in {E}\left({X}\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}\right)\right)$
39 3 38 mpd ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\right)\to \left({Y}\in {E}\left({X}\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}\right)$
40 39 3impia ${⊢}\left({G}\in \mathrm{USGraph}\wedge {X}\in \mathrm{dom}{E}\wedge {Y}\in {E}\left({X}\right)\right)\to \exists {y}\in {V}\phantom{\rule{.4em}{0ex}}{E}\left({X}\right)=\left\{{Y},{y}\right\}$