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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ∖ cdif 3899  ∅c0 4283  𝒫 cpw 4550  {csn 4576  dom cdm 5616  Fun wfun 6475  ‘cfv 6481  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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  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  29615  wlkiswwlks1  29846  wlkiswwlksupgr2  29856  umgrwwlks2on  29936  vdn0conngrumgrv2  30174  eulerpathpr  30218  eulercrct  30220  lfuhgr  35160  loop1cycl  35179  umgr2cycllem  35182  isubgrvtxuhgr  47901  isubgredg  47903  isubgrsubgr  47906  isubgr0uhgr  47910  uhgrimedgi  47927  isuspgrim0lem  47930  isuspgrim0  47931  upgrimwlklem2  47935  upgrimwlklem3  47936  upgrimtrlslem1  47941  clnbgrgrimlem  47970  clnbgrgrim  47971  grimedg  47972