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

Metamath Proof Explorer

Theorem edgval

Description: The edges of a graph. (Contributed by AV, 1-Jan-2020) (Revised by AV, 13-Oct-2020) (Revised by AV, 8-Dec-2021)

Ref Expression
Assertion edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
2 1 rneqd ⊢ ( 𝑔 = 𝐺 → ran ( iEdg ‘ 𝑔 ) = ran ( iEdg ‘ 𝐺 ) )
3 df-edg ⊢ Edg = ( 𝑔 ∈ V ↦ ran ( iEdg ‘ 𝑔 ) )
4 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
5 4 rnex ⊢ ran ( iEdg ‘ 𝐺 ) ∈ V
6 2 3 5 fvmpt ⊢ ( 𝐺 ∈ V → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
7 rn0 ⊢ ran ∅ = ∅
8 7 a1i ⊢ ( ¬ 𝐺 ∈ V → ran ∅ = ∅ )
9 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( iEdg ‘ 𝐺 ) = ∅ )
10 9 rneqd ⊢ ( ¬ 𝐺 ∈ V → ran ( iEdg ‘ 𝐺 ) = ran ∅ )
11 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( Edg ‘ 𝐺 ) = ∅ )
12 8 10 11 3eqtr4rd ⊢ ( ¬ 𝐺 ∈ V → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
13 6 12 pm2.61i ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )