This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uspgrf1oedg

Description: The edge function of a simple pseudograph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020) (Revised by AV, 15-Oct-2020)

Ref Expression
Hypothesis usgrf1o.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion uspgrf1oedg ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸 –1-1-onto→ ( Edg ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 usgrf1o.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 2 1 uspgrf ⊢ ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
4 f1f1orn ⊢ ( 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 )
5 1 rneqi ⊢ ran 𝐸 = ran ( iEdg ‘ 𝐺 )
6 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
7 5 6 eqtr4i ⊢ ran 𝐸 = ( Edg ‘ 𝐺 )
8 f1oeq3 ⊢ ( ran 𝐸 = ( Edg ‘ 𝐺 ) → ( 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 ↔ 𝐸 : dom 𝐸 –1-1-onto→ ( Edg ‘ 𝐺 ) ) )
9 7 8 ax-mp ⊢ ( 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 ↔ 𝐸 : dom 𝐸 –1-1-onto→ ( Edg ‘ 𝐺 ) )
10 4 9 sylib ⊢ ( 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → 𝐸 : dom 𝐸 –1-1-onto→ ( Edg ‘ 𝐺 ) )
11 3 10 syl ⊢ ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸 –1-1-onto→ ( Edg ‘ 𝐺 ) )