# Metamath Proof Explorer

## Theorem umgrpredgv

Description: An edge of a multigraph always connects two vertices. Analogue of umgredgprv . This theorem does not hold for arbitrary pseudographs: if either M or N is a proper class, then { M , N } e. E could still hold ( { M , N } would be either { M } or { N } , see prprc1 or prprc2 , i.e. a loop), but M e. V or N e. V would not be true. (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypotheses upgredg.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
upgredg.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion umgrpredgv ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{M},{N}\right\}\in {E}\right)\to \left({M}\in {V}\wedge {N}\in {V}\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 2 eleq2i ${⊢}\left\{{M},{N}\right\}\in {E}↔\left\{{M},{N}\right\}\in \mathrm{Edg}\left({G}\right)$
4 edgumgr ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{M},{N}\right\}\in \mathrm{Edg}\left({G}\right)\right)\to \left(\left\{{M},{N}\right\}\in 𝒫\mathrm{Vtx}\left({G}\right)\wedge \left|\left\{{M},{N}\right\}\right|=2\right)$
5 3 4 sylan2b ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{M},{N}\right\}\in {E}\right)\to \left(\left\{{M},{N}\right\}\in 𝒫\mathrm{Vtx}\left({G}\right)\wedge \left|\left\{{M},{N}\right\}\right|=2\right)$
6 eqid ${⊢}\left\{{M},{N}\right\}=\left\{{M},{N}\right\}$
7 6 hashprdifel ${⊢}\left|\left\{{M},{N}\right\}\right|=2\to \left({M}\in \left\{{M},{N}\right\}\wedge {N}\in \left\{{M},{N}\right\}\wedge {M}\ne {N}\right)$
8 1 eqcomi ${⊢}\mathrm{Vtx}\left({G}\right)={V}$
9 8 pweqi ${⊢}𝒫\mathrm{Vtx}\left({G}\right)=𝒫{V}$
10 9 eleq2i ${⊢}\left\{{M},{N}\right\}\in 𝒫\mathrm{Vtx}\left({G}\right)↔\left\{{M},{N}\right\}\in 𝒫{V}$
11 prelpw ${⊢}\left({M}\in \left\{{M},{N}\right\}\wedge {N}\in \left\{{M},{N}\right\}\right)\to \left(\left({M}\in {V}\wedge {N}\in {V}\right)↔\left\{{M},{N}\right\}\in 𝒫{V}\right)$
12 11 biimprd ${⊢}\left({M}\in \left\{{M},{N}\right\}\wedge {N}\in \left\{{M},{N}\right\}\right)\to \left(\left\{{M},{N}\right\}\in 𝒫{V}\to \left({M}\in {V}\wedge {N}\in {V}\right)\right)$
13 10 12 syl5bi ${⊢}\left({M}\in \left\{{M},{N}\right\}\wedge {N}\in \left\{{M},{N}\right\}\right)\to \left(\left\{{M},{N}\right\}\in 𝒫\mathrm{Vtx}\left({G}\right)\to \left({M}\in {V}\wedge {N}\in {V}\right)\right)$
14 13 3adant3 ${⊢}\left({M}\in \left\{{M},{N}\right\}\wedge {N}\in \left\{{M},{N}\right\}\wedge {M}\ne {N}\right)\to \left(\left\{{M},{N}\right\}\in 𝒫\mathrm{Vtx}\left({G}\right)\to \left({M}\in {V}\wedge {N}\in {V}\right)\right)$
15 7 14 syl ${⊢}\left|\left\{{M},{N}\right\}\right|=2\to \left(\left\{{M},{N}\right\}\in 𝒫\mathrm{Vtx}\left({G}\right)\to \left({M}\in {V}\wedge {N}\in {V}\right)\right)$
16 15 impcom ${⊢}\left(\left\{{M},{N}\right\}\in 𝒫\mathrm{Vtx}\left({G}\right)\wedge \left|\left\{{M},{N}\right\}\right|=2\right)\to \left({M}\in {V}\wedge {N}\in {V}\right)$
17 5 16 syl ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{M},{N}\right\}\in {E}\right)\to \left({M}\in {V}\wedge {N}\in {V}\right)$