Theorem uhgrfun 29397

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 29393	. 2 ⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
4	3	ffund 6712	1 ⊢ (𝐺 ∈ UHGraph → Fun 𝐸)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ∖ cdif 3903  ∅c0 4287  𝒫 cpw 4563  {csn 4590  dom cdm 5663  Fun wfun 6532  ‘cfv 6538  Vtxcvtx 29327  iEdgciedg 29328  UHGraphcuhgr 29387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-uhgr 29389

This theorem is referenced by:  lpvtx  29399  upgrle2  29436  uhgredgiedgb  29457  uhgriedg0edg0  29458  uhgrvtxedgiedgb  29467  edglnl  29474  numedglnl  29475  uhgr2edg  29539  ushgredgedg  29560  ushgredgedgloop  29562  0uhgrsubgr  29610  uhgrsubgrself  29611  subgruhgrfun  29613  subgruhgredgd  29615  subumgredg2  29616  subupgr  29618  uhgrspansubgrlem  29621  uhgrspansubgr  29622  uhgrspan1  29634  upgrreslem  29635  umgrreslem  29636  upgrres  29637  umgrres  29638  vtxduhgr0e  29809  vtxduhgrun  29814  vtxduhgrfiun  29815  finsumvtxdg2ssteplem1  29876  upgrewlkle2  29937  upgredginwlk  29966  wlkiswwlks1  30197  wlkiswwlksupgr2  30207  usgrwwlks2on  30288  umgrwwlks2on  30289  vdn0conngrumgrv2  30528  eulerpathpr  30572  eulercrct  30574  lfuhgr  35591  loop1cycl  35610  umgr2cycllem  35613  isubgrvtxuhgr  48612  isubgredg  48614  isubgrsubgr  48617  isubgr0uhgr  48621  uhgrimedgi  48638  isuspgrim0lem  48641  isuspgrim0  48642  upgrimwlklem2  48646  upgrimwlklem3  48647  upgrimtrlslem1  48652  clnbgrgrimlem  48681  clnbgrgrim  48682  grimedg  48683