# Metamath Proof Explorer

## Theorem upgredg2vtx

Description: For a vertex incident to an edge there is another vertex incident to the edge in a pseudograph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 5-Dec-2020)

Ref Expression
Hypotheses upgredg.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
upgredg.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion upgredg2vtx ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {C}\in {E}\wedge {A}\in {C}\right)\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{A},{b}\right\}$

### Proof

Step Hyp Ref Expression
1 upgredg.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 upgredg.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 1 2 upgredg ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {C}\in {E}\right)\to \exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{a},{c}\right\}$
4 3 3adant3 ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {C}\in {E}\wedge {A}\in {C}\right)\to \exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{a},{c}\right\}$
5 elpr2elpr ${⊢}\left({a}\in {V}\wedge {c}\in {V}\wedge {A}\in \left\{{a},{c}\right\}\right)\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left\{{a},{c}\right\}=\left\{{A},{b}\right\}$
6 5 3expia ${⊢}\left({a}\in {V}\wedge {c}\in {V}\right)\to \left({A}\in \left\{{a},{c}\right\}\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left\{{a},{c}\right\}=\left\{{A},{b}\right\}\right)$
7 eleq2 ${⊢}{C}=\left\{{a},{c}\right\}\to \left({A}\in {C}↔{A}\in \left\{{a},{c}\right\}\right)$
8 eqeq1 ${⊢}{C}=\left\{{a},{c}\right\}\to \left({C}=\left\{{A},{b}\right\}↔\left\{{a},{c}\right\}=\left\{{A},{b}\right\}\right)$
9 8 rexbidv ${⊢}{C}=\left\{{a},{c}\right\}\to \left(\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{A},{b}\right\}↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left\{{a},{c}\right\}=\left\{{A},{b}\right\}\right)$
10 7 9 imbi12d ${⊢}{C}=\left\{{a},{c}\right\}\to \left(\left({A}\in {C}\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{A},{b}\right\}\right)↔\left({A}\in \left\{{a},{c}\right\}\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left\{{a},{c}\right\}=\left\{{A},{b}\right\}\right)\right)$
11 6 10 syl5ibr ${⊢}{C}=\left\{{a},{c}\right\}\to \left(\left({a}\in {V}\wedge {c}\in {V}\right)\to \left({A}\in {C}\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{A},{b}\right\}\right)\right)$
12 11 com13 ${⊢}{A}\in {C}\to \left(\left({a}\in {V}\wedge {c}\in {V}\right)\to \left({C}=\left\{{a},{c}\right\}\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{A},{b}\right\}\right)\right)$
13 12 3ad2ant3 ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {C}\in {E}\wedge {A}\in {C}\right)\to \left(\left({a}\in {V}\wedge {c}\in {V}\right)\to \left({C}=\left\{{a},{c}\right\}\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{A},{b}\right\}\right)\right)$
14 13 rexlimdvv ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {C}\in {E}\wedge {A}\in {C}\right)\to \left(\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{a},{c}\right\}\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{A},{b}\right\}\right)$
15 4 14 mpd ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {C}\in {E}\wedge {A}\in {C}\right)\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}{C}=\left\{{A},{b}\right\}$