Metamath Proof Explorer

Theorem usgredgprv

Description: In a simple graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 16-Oct-2020) (Proof shortened by AV, 11-Dec-2020)

Ref Expression
Hypotheses usgredg2.e ⊢ E = iEdg ⁡ G
usgredgprv.v ⊢ V = Vtx ⁡ G
Assertion usgredgprv ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → E ⁡ X = M N → M ∈ V ∧ N ∈ V

Proof

Step Hyp Ref Expression
1 usgredg2.e ⊢ E = iEdg ⁡ G
2 usgredgprv.v ⊢ V = Vtx ⁡ G
3 usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph
4 1 2 umgredgprv ⊢ G ∈ UMGraph ∧ X ∈ dom ⁡ E → E ⁡ X = M N → M ∈ V ∧ N ∈ V
5 3 4 sylan ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → E ⁡ X = M N → M ∈ V ∧ N ∈ V