Metamath Proof Explorer

Theorem umgredgprv

Description: In a multigraph, an edge is an unordered pair of vertices. This theorem would not hold for arbitrary hyper-/pseudographs since either M or N could be proper classes ( ( EX ) would be a loop in this case), which are no vertices of course. (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 11-Dec-2020)

Ref Expression
Hypotheses umgrnloopv.e ⊢E=iEdg⁡G
umgredgprv.v ⊢V=Vtx⁡G
Assertion umgredgprv ⊢G∈UMGraph∧X∈dom⁡E→E⁡X=MN→M∈V∧N∈V

Proof

Step Hyp Ref Expression
1 umgrnloopv.e ⊢E=iEdg⁡G
2 umgredgprv.v ⊢V=Vtx⁡G
3 umgruhgr ⊢G∈UMGraph→G∈UHGraph
4 2 1 uhgrss ⊢G∈UHGraph∧X∈dom⁡E→E⁡X⊆V
5 3 4 sylan ⊢G∈UMGraph∧X∈dom⁡E→E⁡X⊆V
6 2 1 umgredg2 ⊢G∈UMGraph∧X∈dom⁡E→E⁡X=2
7 sseq1 ⊢E⁡X=MN→E⁡X⊆V↔MN⊆V
8 fveqeq2 ⊢E⁡X=MN→E⁡X=2↔MN=2
9 7 8 anbi12d ⊢E⁡X=MN→E⁡X⊆V∧E⁡X=2↔MN⊆V∧MN=2
10 eqid ⊢MN=MN
11 10 hashprdifel ⊢MN=2→M∈MN∧N∈MN∧M≠N
12 prssg ⊢M∈MN∧N∈MN→M∈V∧N∈V↔MN⊆V
13 12 3adant3 ⊢M∈MN∧N∈MN∧M≠N→M∈V∧N∈V↔MN⊆V
14 13 biimprd ⊢M∈MN∧N∈MN∧M≠N→MN⊆V→M∈V∧N∈V
15 11 14 syl ⊢MN=2→MN⊆V→M∈V∧N∈V
16 15 impcom ⊢MN⊆V∧MN=2→M∈V∧N∈V
17 9 16 syl6bi ⊢E⁡X=MN→E⁡X⊆V∧E⁡X=2→M∈V∧N∈V
18 17 com12 ⊢E⁡X⊆V∧E⁡X=2→E⁡X=MN→M∈V∧N∈V
19 5 6 18 syl2anc ⊢G∈UMGraph∧X∈dom⁡E→E⁡X=MN→M∈V∧N∈V