Theorem uhgrfun 29213

Description: The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 15-Dec-2020.)

Hypothesis

Ref	Expression
uhgrfun.e	⊢ 𝐸 = (iEdg‘𝐺)

Assertion

Ref	Expression
uhgrfun	⊢ (𝐺 ∈ UHGraph → Fun 𝐸)

Proof of Theorem uhgrfun

Step	Hyp	Ref	Expression
1		eqid 2761	. . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		uhgrfun.e	. . 3 ⊢ 𝐸 = (iEdg‘𝐺)
3	1, 2	uhgrf 29209	. 2 ⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
4	3	ffund 6692	1 ⊢ (𝐺 ∈ UHGraph → Fun 𝐸)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141   ∖ cdif 3901  ∅c0 4285  𝒫 cpw 4554  {csn 4581  dom cdm 5645  Fun wfun 6511  ‘cfv 6517  Vtxcvtx 29143  iEdgciedg 29144  UHGraphcuhgr 29203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-fv 6525  df-uhgr 29205

This theorem is referenced by:  lpvtx  29215  upgrle2  29252  uhgredgiedgb  29273  uhgriedg0edg0  29274  uhgrvtxedgiedgb  29283  edglnl  29290  numedglnl  29291  uhgr2edg  29355  ushgredgedg  29376  ushgredgedgloop  29378  0uhgrsubgr  29426  uhgrsubgrself  29427  subgruhgrfun  29429  subgruhgredgd  29431  subumgredg2  29432  subupgr  29434  uhgrspansubgrlem  29437  uhgrspansubgr  29438  uhgrspan1  29450  upgrreslem  29451  umgrreslem  29452  upgrres  29453  umgrres  29454  vtxduhgr0e  29625  vtxduhgrun  29630  vtxduhgrfiun  29631  finsumvtxdg2ssteplem1  29692  upgrewlkle2  29753  upgredginwlk  29782  wlkiswwlks1  30013  wlkiswwlksupgr2  30023  usgrwwlks2on  30104  umgrwwlks2on  30105  vdn0conngrumgrv2  30344  eulerpathpr  30388  eulercrct  30390  lfuhgr  35432  loop1cycl  35451  umgr2cycllem  35454  isubgrvtxuhgr  48450  isubgredg  48452  isubgrsubgr  48455  isubgr0uhgr  48459  uhgrimedgi  48476  isuspgrim0lem  48479  isuspgrim0  48480  upgrimwlklem2  48484  upgrimwlklem3  48485  upgrimtrlslem1  48490  clnbgrgrimlem  48519  clnbgrgrim  48520  grimedg  48521