Theorem uhgrfun 29645

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 29641	. 2 ⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
4	3	ffund 6715	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 6533  ‘cfv 6539  Vtxcvtx 29575  iEdgciedg 29576  UHGraphcuhgr 29635

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 3900  df-un 3902  df-ss 3915  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 6495  df-fun 6541  df-fn 6542  df-f 6543  df-fv 6547  df-uhgr 29637

This theorem is used by:  lpvtx  29647  upgrle2  29684  uhgredgiedgb  29705  uhgriedg0edg0  29706  uhgrvtxedgiedgb  29715  edglnl  29722  numedglnl  29723  lfuhgr  29727  uhgr2edg  29790  ushgredgedg  29811  ushgredgedgloop  29813  0uhgrsubgr  29861  uhgrsubgrself  29862  subgruhgrfun  29864  subgruhgredgd  29866  subumgredg2  29867  subupgr  29869  uhgrspansubgrlem  29872  uhgrspansubgr  29873  uhgrspan1  29885  upgrreslem  29886  umgrreslem  29887  upgrres  29888  umgrres  29889  vtxduhgr0e  30060  vtxduhgrun  30065  vtxduhgrfiun  30066  finsumvtxdg2ssteplem1  30127  upgrewlkle2  30188  upgredginwlk  30217  wlkiswwlks1  30457  wlkiswwlksupgr2  30467  usgrwwlks2on  30548  umgrwwlks2on  30549  loop1cycl  30745  umgr2cycllem  30747  vdn0conngrumgrv2  30798  eulerpathpr  30842  eulercrct  30844  isubgrvtxuhgr  48963  isubgredg  48965  isubgrsubgr  48968  isubgr0uhgr  48972  uhgrimedgi  48989  isuspgrim0lem  48992  isuspgrim0  48993  upgrimwlklem2  48997  upgrimwlklem3  48998  upgrimtrlslem1  49003  clnbgrgrimlem  49032  clnbgrgrim  49033  grimedg  49034