Theorem edgval 25941

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		df-edg 25940	. . . 4 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
2	1	a1i 11	. . 3 ⊢ (𝐺 ∈ V → Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔)))
3		fveq2 6191	. . . . 5 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
4	3	rneqd 5353	. . . 4 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
5	4	adantl 482	. . 3 ⊢ ((𝐺 ∈ V ∧ 𝑔 = 𝐺) → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
6		id 22	. . 3 ⊢ (𝐺 ∈ V → 𝐺 ∈ V)
7		fvex 6201	. . . . 5 ⊢ (iEdg‘𝐺) ∈ V
8	7	rnex 7100	. . . 4 ⊢ ran (iEdg‘𝐺) ∈ V
9	8	a1i 11	. . 3 ⊢ (𝐺 ∈ V → ran (iEdg‘𝐺) ∈ V)
10	2, 5, 6, 9	fvmptd 6288	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
11		rn0 5377	. . . 4 ⊢ ran ∅ = ∅
12	11	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
13		fvprc 6185	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
14	13	rneqd 5353	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
15		fvprc 6185	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
16	12, 14, 15	3eqtr4rd 2667	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
17	10, 16	pm2.61i 176	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1483   ∈ wcel 1990  Vcvv 3200  ∅c0 3915   ↦ cmpt 4729  ran crn 5115  ‘cfv 5888  iEdgciedg 25875  Edgcedg 25939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fv 5896  df-edg 25940

This theorem is referenced by:  iedgedg  25943  edgopval  25944  edgstruct  25946  edgiedgb  25947  edg0iedg0  25949  uhgredgn0  26023  upgredgss  26027  umgredgss  26028  edgupgr  26029  uhgrvtxedgiedgb  26031  upgredg  26032  usgredgss  26054  ausgrumgri  26062  ausgrusgri  26063  uspgrf1oedg  26068  uspgrupgrushgr  26072  usgrumgruspgr  26075  usgruspgrb  26076  usgrf1oedg  26099  uhgr2edg  26100  usgrsizedg  26107  usgredg3  26108  ushgredgedg  26121  ushgredgedgloop  26123  usgr1e  26137  edg0usgr  26145  usgr1v0edg  26149  usgrexmpledg  26154  subgrprop3  26168  0grsubgr  26170  0uhgrsubgr  26171  subgruhgredgd  26176  uhgrspansubgrlem  26182  uhgrspan1  26195  upgrres1  26205  usgredgffibi  26216  dfnbgr3  26236  nbupgrres  26266  usgrnbcnvfv  26267  cplgrop  26333  cusgrexi  26339  structtocusgr  26342  cusgrsize  26350  1loopgredg  26397  1egrvtxdg0  26407  umgr2v2eedg  26420  edginwlk  26530  wlkl1loop  26534  wlkvtxedg  26540  uspgr2wlkeq  26542  wlkiswwlks1  26753  wlkiswwlks2lem4  26758  wlkiswwlks2lem5  26759  wlkiswwlks2  26761  wlkiswwlksupgr2  26763  2pthon3v  26839  umgrwwlks2on  26850  clwlkclwwlk  26903  clwlksfclwwlk  26962