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 = M N → 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 = M N → E ⁡ X ⊆ V ↔ M N ⊆ V
8 fveqeq2 ⊢ E ⁡ X = M N → E ⁡ X = 2 ↔ M N = 2
9 7 8 anbi12d ⊢ E ⁡ X = M N → E ⁡ X ⊆ V ∧ E ⁡ X = 2 ↔ M N ⊆ V ∧ M N = 2
10 eqid ⊢ M N = M N
11 10 hashprdifel ⊢ M N = 2 → M ∈ M N ∧ N ∈ M N ∧ M ≠ N
12 prssg ⊢ M ∈ M N ∧ N ∈ M N → M ∈ V ∧ N ∈ V ↔ M N ⊆ V
13 12 3adant3 ⊢ M ∈ M N ∧ N ∈ M N ∧ M ≠ N → M ∈ V ∧ N ∈ V ↔ M N ⊆ V
14 13 biimprd ⊢ M ∈ M N ∧ N ∈ M N ∧ M ≠ N → M N ⊆ V → M ∈ V ∧ N ∈ V
15 11 14 syl ⊢ M N = 2 → M N ⊆ V → M ∈ V ∧ N ∈ V
16 15 impcom ⊢ M N ⊆ V ∧ M N = 2 → M ∈ V ∧ N ∈ V
17 9 16 biimtrdi ⊢ E ⁡ X = M N → E ⁡ X ⊆ V ∧ E ⁡ X = 2 → M ∈ V ∧ N ∈ V
18 17 com12 ⊢ E ⁡ X ⊆ V ∧ E ⁡ X = 2 → E ⁡ X = M N → M ∈ V ∧ N ∈ V
19 5 6 18 syl2anc ⊢ G ∈ UMGraph ∧ X ∈ dom ⁡ E → E ⁡ X = M N → M ∈ V ∧ N ∈ V