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=Vtx⁡G
upgredg.e ⊢E=Edg⁡G
Assertion umgrpredgv ⊢G∈UMGraph∧MN∈E→M∈V∧N∈V

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢V=Vtx⁡G
2 upgredg.e ⊢E=Edg⁡G
3 2 eleq2i ⊢MN∈E↔MN∈Edg⁡G
4 edgumgr ⊢G∈UMGraph∧MN∈Edg⁡G→MN∈𝒫Vtx⁡G∧MN=2
5 3 4 sylan2b ⊢G∈UMGraph∧MN∈E→MN∈𝒫Vtx⁡G∧MN=2
6 eqid ⊢MN=MN
7 6 hashprdifel ⊢MN=2→M∈MN∧N∈MN∧M≠N
8 1 eqcomi ⊢Vtx⁡G=V
9 8 pweqi ⊢𝒫Vtx⁡G=𝒫V
10 9 eleq2i ⊢MN∈𝒫Vtx⁡G↔MN∈𝒫V
11 prelpw ⊢M∈MN∧N∈MN→M∈V∧N∈V↔MN∈𝒫V
12 11 biimprd ⊢M∈MN∧N∈MN→MN∈𝒫V→M∈V∧N∈V
13 10 12 syl5bi ⊢M∈MN∧N∈MN→MN∈𝒫Vtx⁡G→M∈V∧N∈V
14 13 3adant3 ⊢M∈MN∧N∈MN∧M≠N→MN∈𝒫Vtx⁡G→M∈V∧N∈V
15 7 14 syl ⊢MN=2→MN∈𝒫Vtx⁡G→M∈V∧N∈V
16 15 impcom ⊢MN∈𝒫Vtx⁡G∧MN=2→M∈V∧N∈V
17 5 16 syl ⊢G∈UMGraph∧MN∈E→M∈V∧N∈V