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

Metamath Proof Explorer

Theorem usgrf1oedg

Description: The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020)

Ref Expression
Hypotheses usgrf1oedg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
usgrf1oedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion usgrf1oedg ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1-onto→ 𝐸 )

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 usgrf1oedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 3 1 usgrf ⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5 f1f1orn ⊢ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )
6 4 5 syl ⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )
7 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
8 7 a1i ⊢ ( 𝐺 ∈ USGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
9 1 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐼
10 9 rneqi ⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼
11 8 10 eqtrdi ⊢ ( 𝐺 ∈ USGraph → ( Edg ‘ 𝐺 ) = ran 𝐼 )
12 2 11 eqtrid ⊢ ( 𝐺 ∈ USGraph → 𝐸 = ran 𝐼 )
13 12 f1oeq3d ⊢ ( 𝐺 ∈ USGraph → ( 𝐼 : dom 𝐼 –1-1-onto→ 𝐸 ↔ 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 ) )
14 6 13 mpbird ⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1-onto→ 𝐸 )