Theorem uhgrfun 29677

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ∖ cdif 4048  ∅c0 4281  𝒫 cpw 4560  {csn 4588  dom cdm 5656  Fun wfun 6555  ‘cfv 6561  Vtxcvtx 29607  iEdgciedg 29608  UHGraphcuhgr 29667

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5264

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-uhgr 29669

This theorem is used by:  lpvtx  29679  upgrle2  29716  uhgredgiedgb  29737  uhgriedg0edg0  29738  uhgrvtxedgiedgb  29747  edglnl  29754  numedglnl  29755  lfuhgr  29759  uhgr2edg  29822  ushgredgedg  29843  ushgredgedgloop  29845  0uhgrsubgr  29893  uhgrsubgrself  29894  subgruhgrfun  29896  subgruhgredgd  29898  subumgredg2  29899  subupgr  29901  uhgrspansubgrlem  29904  uhgrspansubgr  29905  uhgrspan1  29917  upgrreslem  29918  umgrreslem  29919  upgrres  29920  umgrres  29921  vtxduhgr0e  30092  vtxduhgrun  30097  vtxduhgrfiun  30098  finsumvtxdg2ssteplem1  30159  upgrewlkle2  30220  upgredginwlk  30249  wlkiswwlks1  30489  wlkiswwlksupgr2  30499  usgrwwlks2on  30580  umgrwwlks2on  30581  loop1cycl  30777  umgr2cycllem  30779  vdn0conngrumgrv2  30830  eulerpathpr  30874  eulercrct  30876  isubgrvtxuhgr  49177  isubgredg  49179  isubgrsubgr  49182  isubgr0uhgr  49186  uhgrimedgi  49203  isuspgrim0lem  49206  isuspgrim0  49207  upgrimwlklem2  49211  upgrimwlklem3  49212  upgrimtrlslem1  49217  clnbgrgrimlem  49246  clnbgrgrim  49247  grimedg  49248