MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  edgval Structured version   Visualization version   GIF version

Theorem edgval 25935
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.
StepHypRef Expression
1 df-edg 25934 . . . 4 Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
21a1i 11 . . 3 (𝐺 ∈ V → Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔)))
3 fveq2 6189 . . . . 5 (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
43rneqd 5351 . . . 4 (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
54adantl 482 . . 3 ((𝐺 ∈ V ∧ 𝑔 = 𝐺) → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
6 id 22 . . 3 (𝐺 ∈ V → 𝐺 ∈ V)
7 fvex 6199 . . . . 5 (iEdg‘𝐺) ∈ V
87rnex 7097 . . . 4 ran (iEdg‘𝐺) ∈ V
98a1i 11 . . 3 (𝐺 ∈ V → ran (iEdg‘𝐺) ∈ V)
102, 5, 6, 9fvmptd 6286 . 2 (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
11 rn0 5375 . . . 4 ran ∅ = ∅
1211a1i 11 . . 3 𝐺 ∈ V → ran ∅ = ∅)
13 fvprc 6183 . . . 4 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
1413rneqd 5351 . . 3 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
15 fvprc 6183 . . 3 𝐺 ∈ V → (Edg‘𝐺) = ∅)
1612, 14, 153eqtr4rd 2666 . 2 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
1710, 16pm2.61i 176 1 (Edg‘𝐺) = ran (iEdg‘𝐺)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1482  wcel 1989  Vcvv 3198  c0 3913  cmpt 4727  ran crn 5113  cfv 5886  iEdgciedg 25869  Edgcedg 25933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-mpt 4728  df-id 5022  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-iota 5849  df-fun 5888  df-fv 5894  df-edg 25934
This theorem is referenced by:  iedgedg  25937  edgopval  25938  edgstruct  25940  edgiedgb  25941  edg0iedg0  25943  uhgredgn0  26017  upgredgss  26021  umgredgss  26022  edgupgr  26023  uhgrvtxedgiedgb  26025  upgredg  26026  usgredgss  26048  ausgrumgri  26056  ausgrusgri  26057  uspgrf1oedg  26062  uspgrupgrushgr  26066  usgrumgruspgr  26069  usgruspgrb  26070  usgrf1oedg  26093  uhgr2edg  26094  usgrsizedg  26101  usgredg3  26102  ushgredgedg  26115  ushgredgedgloop  26117  usgr1e  26131  edg0usgr  26139  usgr1v0edg  26143  usgrexmpledg  26148  subgrprop3  26162  0grsubgr  26164  0uhgrsubgr  26165  subgruhgredgd  26170  uhgrspansubgrlem  26176  uhgrspan1  26189  upgrres1  26199  usgredgffibi  26210  dfnbgr3  26230  nbupgrres  26260  usgrnbcnvfv  26261  cplgrop  26327  cusgrexi  26333  structtocusgr  26336  cusgrsize  26344  1loopgredg  26391  1egrvtxdg0  26401  umgr2v2eedg  26414  edginwlk  26524  wlkl1loop  26528  wlkvtxedg  26534  uspgr2wlkeq  26536  wlkiswwlks1  26747  wlkiswwlks2lem4  26752  wlkiswwlks2lem5  26753  wlkiswwlks2  26755  wlkiswwlksupgr2  26757  2pthon3v  26833  umgrwwlks2on  26844  clwlkclwwlk  26897  clwlksfclwwlk  26955
  Copyright terms: Public domain W3C validator