Theorem edgval 27322

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

Assertion

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

Proof of Theorem edgval

Dummy variable 𝑔 is distinct from all other variables.

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

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ∅c0 4253  ran crn 5581  ‘cfv 6418  iEdgciedg 27270  Edgcedg 27320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fv 6426  df-edg 27321

This theorem is referenced by:  iedgedg  27323  edgopval  27324  edgstruct  27326  edgiedgb  27327  edg0iedg0  27328  uhgredgn0  27401  upgredgss  27405  umgredgss  27406  edgupgr  27407  uhgrvtxedgiedgb  27409  upgredg  27410  usgredgss  27432  ausgrumgri  27440  ausgrusgri  27441  uspgrf1oedg  27446  uspgrupgrushgr  27450  usgrumgruspgr  27453  usgruspgrb  27454  usgrf1oedg  27477  uhgr2edg  27478  usgrsizedg  27485  usgredg3  27486  ushgredgedg  27499  ushgredgedgloop  27501  usgr1e  27515  edg0usgr  27523  usgr1v0edg  27527  usgrexmpledg  27532  subgrprop3  27546  0grsubgr  27548  0uhgrsubgr  27549  subgruhgredgd  27554  uhgrspansubgrlem  27560  uhgrspan1  27573  upgrres1  27583  usgredgffibi  27594  dfnbgr3  27608  nbupgrres  27634  usgrnbcnvfv  27635  cplgrop  27707  cusgrexi  27713  structtocusgr  27716  cusgrsize  27724  1loopgredg  27771  1egrvtxdg0  27781  umgr2v2eedg  27794  edginwlk  27904  wlkl1loop  27907  wlkvtxedg  27913  uspgr2wlkeq  27915  wlkiswwlks1  28133  wlkiswwlks2lem4  28138  wlkiswwlks2lem5  28139  wlkiswwlks2  28141  wlkiswwlksupgr2  28143  2pthon3v  28209  umgrwwlks2on  28223  clwlkclwwlk  28267  lfuhgr  32979  loop1cycl  32999  isomushgr  45166  ushrisomgr  45181