Theorem uhgrfun 29045

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ∖ cdif 3923  ∅c0 4308  𝒫 cpw 4575  {csn 4601  dom cdm 5654  Fun wfun 6525  ‘cfv 6531  Vtxcvtx 28975  iEdgciedg 28976  UHGraphcuhgr 29035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-uhgr 29037

This theorem is referenced by:  lpvtx  29047  upgrle2  29084  uhgredgiedgb  29105  uhgriedg0edg0  29106  uhgrvtxedgiedgb  29115  edglnl  29122  numedglnl  29123  uhgr2edg  29187  ushgredgedg  29208  ushgredgedgloop  29210  0uhgrsubgr  29258  uhgrsubgrself  29259  subgruhgrfun  29261  subgruhgredgd  29263  subumgredg2  29264  subupgr  29266  uhgrspansubgrlem  29269  uhgrspansubgr  29270  uhgrspan1  29282  upgrreslem  29283  umgrreslem  29284  upgrres  29285  umgrres  29286  vtxduhgr0e  29458  vtxduhgrun  29463  vtxduhgrfiun  29464  finsumvtxdg2ssteplem1  29525  upgrewlkle2  29586  upgredginwlk  29616  wlkiswwlks1  29849  wlkiswwlksupgr2  29859  umgrwwlks2on  29939  vdn0conngrumgrv2  30177  eulerpathpr  30221  eulercrct  30223  lfuhgr  35140  loop1cycl  35159  umgr2cycllem  35162  isubgrvtxuhgr  47877  isubgredg  47879  isubgrsubgr  47882  isubgr0uhgr  47886  uhgrimedgi  47903  isuspgrim0lem  47906  isuspgrim0  47907  upgrimwlklem2  47911  upgrimwlklem3  47912  upgrimtrlslem1  47917  clnbgrgrimlem  47946  clnbgrgrim  47947  grimedg  47948