Theorem uhgrfun 29531

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ∖ cdif 3899  ∅c0 4282  𝒫 cpw 4560  {csn 4587  dom cdm 5659  Fun wfun 6531  ‘cfv 6537  Vtxcvtx 29461  iEdgciedg 29462  UHGraphcuhgr 29521

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 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-uhgr 29523

This theorem is used by:  lpvtx  29533  upgrle2  29570  uhgredgiedgb  29591  uhgriedg0edg0  29592  uhgrvtxedgiedgb  29601  edglnl  29608  numedglnl  29609  lfuhgr  29613  uhgr2edg  29676  ushgredgedg  29697  ushgredgedgloop  29699  0uhgrsubgr  29747  uhgrsubgrself  29748  subgruhgrfun  29750  subgruhgredgd  29752  subumgredg2  29753  subupgr  29755  uhgrspansubgrlem  29758  uhgrspansubgr  29759  uhgrspan1  29771  upgrreslem  29772  umgrreslem  29773  upgrres  29774  umgrres  29775  vtxduhgr0e  29946  vtxduhgrun  29951  vtxduhgrfiun  29952  finsumvtxdg2ssteplem1  30013  upgrewlkle2  30074  upgredginwlk  30103  wlkiswwlks1  30343  wlkiswwlksupgr2  30353  usgrwwlks2on  30434  umgrwwlks2on  30435  loop1cycl  30631  umgr2cycllem  30633  vdn0conngrumgrv2  30684  eulerpathpr  30728  eulercrct  30730  isubgrvtxuhgr  48788  isubgredg  48790  isubgrsubgr  48793  isubgr0uhgr  48797  uhgrimedgi  48814  isuspgrim0lem  48817  isuspgrim0  48818  upgrimwlklem2  48822  upgrimwlklem3  48823  upgrimtrlslem1  48828  clnbgrgrimlem  48857  clnbgrgrim  48858  grimedg  48859