Theorem uhgrfun 29325

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145   ∖ cdif 3904  ∅c0 4288  𝒫 cpw 4558  {csn 4585  dom cdm 5652  Fun wfun 6519  ‘cfv 6525  Vtxcvtx 29255  iEdgciedg 29256  UHGraphcuhgr 29315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533  df-uhgr 29317

This theorem is referenced by:  lpvtx  29327  upgrle2  29364  uhgredgiedgb  29385  uhgriedg0edg0  29386  uhgrvtxedgiedgb  29395  edglnl  29402  numedglnl  29403  uhgr2edg  29467  ushgredgedg  29488  ushgredgedgloop  29490  0uhgrsubgr  29538  uhgrsubgrself  29539  subgruhgrfun  29541  subgruhgredgd  29543  subumgredg2  29544  subupgr  29546  uhgrspansubgrlem  29549  uhgrspansubgr  29550  uhgrspan1  29562  upgrreslem  29563  umgrreslem  29564  upgrres  29565  umgrres  29566  vtxduhgr0e  29737  vtxduhgrun  29742  vtxduhgrfiun  29743  finsumvtxdg2ssteplem1  29804  upgrewlkle2  29865  upgredginwlk  29894  wlkiswwlks1  30125  wlkiswwlksupgr2  30135  usgrwwlks2on  30216  umgrwwlks2on  30217  vdn0conngrumgrv2  30456  eulerpathpr  30500  eulercrct  30502  lfuhgr  35481  loop1cycl  35500  umgr2cycllem  35503  isubgrvtxuhgr  48484  isubgredg  48486  isubgrsubgr  48489  isubgr0uhgr  48493  uhgrimedgi  48510  isuspgrim0lem  48513  isuspgrim0  48514  upgrimwlklem2  48518  upgrimwlklem3  48519  upgrimtrlslem1  48524  clnbgrgrimlem  48553  clnbgrgrim  48554  grimedg  48555