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 ‘ 𝐺 )