Theorem uhgrfun 29046

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 2733	. . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		uhgrfun.e	. . 3 ⊢ 𝐸 = (iEdg‘𝐺)
3	1, 2	uhgrf 29042	. 2 ⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
4	3	ffund 6660	1 ⊢ (𝐺 ∈ UHGraph → Fun 𝐸)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ∖ cdif 3895  ∅c0 4282  𝒫 cpw 4549  {csn 4575  dom cdm 5619  Fun wfun 6480  ‘cfv 6486  Vtxcvtx 28976  iEdgciedg 28977  UHGraphcuhgr 29036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-uhgr 29038

This theorem is referenced by:  lpvtx  29048  upgrle2  29085  uhgredgiedgb  29106  uhgriedg0edg0  29107  uhgrvtxedgiedgb  29116  edglnl  29123  numedglnl  29124  uhgr2edg  29188  ushgredgedg  29209  ushgredgedgloop  29211  0uhgrsubgr  29259  uhgrsubgrself  29260  subgruhgrfun  29262  subgruhgredgd  29264  subumgredg2  29265  subupgr  29267  uhgrspansubgrlem  29270  uhgrspansubgr  29271  uhgrspan1  29283  upgrreslem  29284  umgrreslem  29285  upgrres  29286  umgrres  29287  vtxduhgr0e  29459  vtxduhgrun  29464  vtxduhgrfiun  29465  finsumvtxdg2ssteplem1  29526  upgrewlkle2  29587  upgredginwlk  29616  wlkiswwlks1  29847  wlkiswwlksupgr2  29857  usgrwwlks2on  29938  umgrwwlks2on  29939  vdn0conngrumgrv2  30178  eulerpathpr  30222  eulercrct  30224  lfuhgr  35183  loop1cycl  35202  umgr2cycllem  35205  isubgrvtxuhgr  47989  isubgredg  47991  isubgrsubgr  47994  isubgr0uhgr  47998  uhgrimedgi  48015  isuspgrim0lem  48018  isuspgrim0  48019  upgrimwlklem2  48023  upgrimwlklem3  48024  upgrimtrlslem1  48029  clnbgrgrimlem  48058  clnbgrgrim  48059  grimedg  48060