Theorem uhgrfun 29101

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ∖ cdif 3973  ∅c0 4352  𝒫 cpw 4622  {csn 4648  dom cdm 5700  Fun wfun 6567  ‘cfv 6573  Vtxcvtx 29031  iEdgciedg 29032  UHGraphcuhgr 29091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-uhgr 29093

This theorem is referenced by:  lpvtx  29103  upgrle2  29140  uhgredgiedgb  29161  uhgriedg0edg0  29162  uhgrvtxedgiedgb  29171  edglnl  29178  numedglnl  29179  uhgr2edg  29243  ushgredgedg  29264  ushgredgedgloop  29266  0uhgrsubgr  29314  uhgrsubgrself  29315  subgruhgrfun  29317  subgruhgredgd  29319  subumgredg2  29320  subupgr  29322  uhgrspansubgrlem  29325  uhgrspansubgr  29326  uhgrspan1  29338  upgrreslem  29339  umgrreslem  29340  upgrres  29341  umgrres  29342  vtxduhgr0e  29514  vtxduhgrun  29519  vtxduhgrfiun  29520  finsumvtxdg2ssteplem1  29581  upgrewlkle2  29642  upgredginwlk  29672  wlkiswwlks1  29900  wlkiswwlksupgr2  29910  umgrwwlks2on  29990  vdn0conngrumgrv2  30228  eulerpathpr  30272  eulercrct  30274  lfuhgr  35085  loop1cycl  35105  umgr2cycllem  35108  isubgrvtxuhgr  47736  isubgrsubgr  47739  isubgr0uhgr  47743  isuspgrim0lem  47755  isuspgrim0  47756  clnbgrgrimlem  47785  clnbgrgrim  47786  grimedg  47787