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 ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{ran}\mathrm{iEdg}\left({G}\right)$

Proof

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