Theorem uhgrfun 29649

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ∖ cdif 4045  ∅c0 4278  𝒫 cpw 4556  {csn 4584  dom cdm 5650  Fun wfun 6532  ‘cfv 6538  Vtxcvtx 29579  iEdgciedg 29580  UHGraphcuhgr 29639

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-uhgr 29641

This theorem is used by:  lpvtx  29651  upgrle2  29688  uhgredgiedgb  29709  uhgriedg0edg0  29710  uhgrvtxedgiedgb  29719  edglnl  29726  numedglnl  29727  lfuhgr  29731  uhgr2edg  29794  ushgredgedg  29815  ushgredgedgloop  29817  0uhgrsubgr  29865  uhgrsubgrself  29866  subgruhgrfun  29868  subgruhgredgd  29870  subumgredg2  29871  subupgr  29873  uhgrspansubgrlem  29876  uhgrspansubgr  29877  uhgrspan1  29889  upgrreslem  29890  umgrreslem  29891  upgrres  29892  umgrres  29893  vtxduhgr0e  30064  vtxduhgrun  30069  vtxduhgrfiun  30070  finsumvtxdg2ssteplem1  30131  upgrewlkle2  30192  upgredginwlk  30221  wlkiswwlks1  30461  wlkiswwlksupgr2  30471  usgrwwlks2on  30552  umgrwwlks2on  30553  loop1cycl  30749  umgr2cycllem  30751  vdn0conngrumgrv2  30802  eulerpathpr  30846  eulercrct  30848  isubgrvtxuhgr  49055  isubgredg  49057  isubgrsubgr  49060  isubgr0uhgr  49064  uhgrimedgi  49081  isuspgrim0lem  49084  isuspgrim0  49085  upgrimwlklem2  49089  upgrimwlklem3  49090  upgrimtrlslem1  49095  clnbgrgrimlem  49124  clnbgrgrim  49125  grimedg  49126