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 (G) = ran iEdg (G)$

Step	Hyp	Ref	Expression
1		fveq2	$⊢ g = G \to iEdg (g) = iEdg (G)$
2	1	rneqd	$⊢ g = G \to ran iEdg (g) = ran iEdg (G)$
3		df-edg	$⊢ Edg = (g \in V ⟼ ran iEdg (g))$
4		fvex	$⊢ iEdg (G) \in V$
5	4	rnex	$⊢ ran iEdg (G) \in V$
6	2 3 5	fvmpt	$⊢ G \in V \to Edg (G) = ran iEdg (G)$
7		rn0	$⊢ ran \emptyset = \emptyset$
8	7	a1i	$⊢ \neg G \in V \to ran \emptyset = \emptyset$
9		fvprc	$⊢ \neg G \in V \to iEdg (G) = \emptyset$
10	9	rneqd	$⊢ \neg G \in V \to ran iEdg (G) = ran \emptyset$
11		fvprc	$⊢ \neg G \in V \to Edg (G) = \emptyset$
12	8 10 11	3eqtr4rd	$⊢ \neg G \in V \to Edg (G) = ran iEdg (G)$
13	6 12	pm2.61i	$⊢ Edg (G) = ran iEdg (G)$

Metamath Proof Explorer