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 usgrnloop0
Description: A simple graph has no loops. (Contributed by Alexander van der Vekens , 6-Dec-2017) (Revised by AV , 17-Oct-2020) (Proof shortened by AV , 11-Dec-2020)
Ref
Expression
Hypothesis
usgrnloopv.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion
usgrnloop0 ⊢ ( 𝐺 ∈ USGraph → { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } } = ∅ )
Proof
Step
Hyp
Ref
Expression
1
usgrnloopv.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2
usgrumgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
3
1
umgrnloop0 ⊢ ( 𝐺 ∈ UMGraph → { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } } = ∅ )
4
2 3
syl ⊢ ( 𝐺 ∈ USGraph → { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } } = ∅ )