Theorem uhgrfun 29453

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ∖ cdif 3905  ∅c0 4289  𝒫 cpw 4567  {csn 4594  dom cdm 5666  Fun wfun 6537  ‘cfv 6543  Vtxcvtx 29383  iEdgciedg 29384  UHGraphcuhgr 29443

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 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-uhgr 29445

This theorem is used by:  lpvtx  29455  upgrle2  29492  uhgredgiedgb  29513  uhgriedg0edg0  29514  uhgrvtxedgiedgb  29523  edglnl  29530  numedglnl  29531  uhgr2edg  29595  ushgredgedg  29616  ushgredgedgloop  29618  0uhgrsubgr  29666  uhgrsubgrself  29667  subgruhgrfun  29669  subgruhgredgd  29671  subumgredg2  29672  subupgr  29674  uhgrspansubgrlem  29677  uhgrspansubgr  29678  uhgrspan1  29690  upgrreslem  29691  umgrreslem  29692  upgrres  29693  umgrres  29694  vtxduhgr0e  29865  vtxduhgrun  29870  vtxduhgrfiun  29871  finsumvtxdg2ssteplem1  29932  upgrewlkle2  29993  upgredginwlk  30022  wlkiswwlks1  30253  wlkiswwlksupgr2  30263  usgrwwlks2on  30344  umgrwwlks2on  30345  vdn0conngrumgrv2  30584  eulerpathpr  30628  eulercrct  30630  lfuhgr  35631  loop1cycl  35650  umgr2cycllem  35653  isubgrvtxuhgr  48670  isubgredg  48672  isubgrsubgr  48675  isubgr0uhgr  48679  uhgrimedgi  48696  isuspgrim0lem  48699  isuspgrim0  48700  upgrimwlklem2  48704  upgrimwlklem3  48705  upgrimtrlslem1  48710  clnbgrgrimlem  48739  clnbgrgrim  48740  grimedg  48741