Theorem uhgrfun 29626

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ∖ cdif 3896  ∅c0 4279  𝒫 cpw 4557  {csn 4584  dom cdm 5651  Fun wfun 6525  ‘cfv 6531  Vtxcvtx 29556  iEdgciedg 29557  UHGraphcuhgr 29616

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-uhgr 29618

This theorem is used by:  lpvtx  29628  upgrle2  29665  uhgredgiedgb  29686  uhgriedg0edg0  29687  uhgrvtxedgiedgb  29696  edglnl  29703  numedglnl  29704  lfuhgr  29708  uhgr2edg  29771  ushgredgedg  29792  ushgredgedgloop  29794  0uhgrsubgr  29842  uhgrsubgrself  29843  subgruhgrfun  29845  subgruhgredgd  29847  subumgredg2  29848  subupgr  29850  uhgrspansubgrlem  29853  uhgrspansubgr  29854  uhgrspan1  29866  upgrreslem  29867  umgrreslem  29868  upgrres  29869  umgrres  29870  vtxduhgr0e  30041  vtxduhgrun  30046  vtxduhgrfiun  30047  finsumvtxdg2ssteplem1  30108  upgrewlkle2  30169  upgredginwlk  30198  wlkiswwlks1  30438  wlkiswwlksupgr2  30448  usgrwwlks2on  30529  umgrwwlks2on  30530  loop1cycl  30726  umgr2cycllem  30728  vdn0conngrumgrv2  30779  eulerpathpr  30823  eulercrct  30825  isubgrvtxuhgr  48906  isubgredg  48908  isubgrsubgr  48911  isubgr0uhgr  48915  uhgrimedgi  48932  isuspgrim0lem  48935  isuspgrim0  48936  upgrimwlklem2  48940  upgrimwlklem3  48941  upgrimtrlslem1  48946  clnbgrgrimlem  48975  clnbgrgrim  48976  grimedg  48977