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 usgrf1
Description: The edge function of a simple graph is a one to one function.
(Contributed by Alexander van der Vekens , 18-Nov-2017) (Revised by AV , 15-Oct-2020)
Ref
Expression
Hypothesis
usgrf1o.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion
usgrf1 ⊢ ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸 –1-1 → ran 𝐸 )
Proof
Step
Hyp
Ref
Expression
1
usgrf1o.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2
1
usgrf1o ⊢ ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸 –1-1 -onto → ran 𝐸 )
3
f1of1 ⊢ ( 𝐸 : dom 𝐸 –1-1 -onto → ran 𝐸 → 𝐸 : dom 𝐸 –1-1 → ran 𝐸 )
4
2 3
syl ⊢ ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸 –1-1 → ran 𝐸 )