Theorem uhgrfun 29151

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∖ cdif 3900  ∅c0 4287  𝒫 cpw 4556  {csn 4582  dom cdm 5632  Fun wfun 6494  ‘cfv 6500  Vtxcvtx 29081  iEdgciedg 29082  UHGraphcuhgr 29141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-uhgr 29143

This theorem is referenced by:  lpvtx  29153  upgrle2  29190  uhgredgiedgb  29211  uhgriedg0edg0  29212  uhgrvtxedgiedgb  29221  edglnl  29228  numedglnl  29229  uhgr2edg  29293  ushgredgedg  29314  ushgredgedgloop  29316  0uhgrsubgr  29364  uhgrsubgrself  29365  subgruhgrfun  29367  subgruhgredgd  29369  subumgredg2  29370  subupgr  29372  uhgrspansubgrlem  29375  uhgrspansubgr  29376  uhgrspan1  29388  upgrreslem  29389  umgrreslem  29390  upgrres  29391  umgrres  29392  vtxduhgr0e  29564  vtxduhgrun  29569  vtxduhgrfiun  29570  finsumvtxdg2ssteplem1  29631  upgrewlkle2  29692  upgredginwlk  29721  wlkiswwlks1  29952  wlkiswwlksupgr2  29962  usgrwwlks2on  30043  umgrwwlks2on  30044  vdn0conngrumgrv2  30283  eulerpathpr  30327  eulercrct  30329  lfuhgr  35331  loop1cycl  35350  umgr2cycllem  35353  isubgrvtxuhgr  48221  isubgredg  48223  isubgrsubgr  48226  isubgr0uhgr  48230  uhgrimedgi  48247  isuspgrim0lem  48250  isuspgrim0  48251  upgrimwlklem2  48255  upgrimwlklem3  48256  upgrimtrlslem1  48261  clnbgrgrimlem  48290  clnbgrgrim  48291  grimedg  48292