This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Undirected simple graphs 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 ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
usgredgprv.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion
usgredgprv ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
Proof
Step
Hyp
Ref
Expression
1
usgredg2.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2
usgredgprv.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3
usgrumgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
4
1 2
umgredgprv ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
5
3 4
sylan ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )