Theorem uhgrfun 29097

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   ∖ cdif 3959  ∅c0 4338  𝒫 cpw 4604  {csn 4630  dom cdm 5688  Fun wfun 6556  ‘cfv 6562  Vtxcvtx 29027  iEdgciedg 29028  UHGraphcuhgr 29087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-uhgr 29089

This theorem is referenced by:  lpvtx  29099  upgrle2  29136  uhgredgiedgb  29157  uhgriedg0edg0  29158  uhgrvtxedgiedgb  29167  edglnl  29174  numedglnl  29175  uhgr2edg  29239  ushgredgedg  29260  ushgredgedgloop  29262  0uhgrsubgr  29310  uhgrsubgrself  29311  subgruhgrfun  29313  subgruhgredgd  29315  subumgredg2  29316  subupgr  29318  uhgrspansubgrlem  29321  uhgrspansubgr  29322  uhgrspan1  29334  upgrreslem  29335  umgrreslem  29336  upgrres  29337  umgrres  29338  vtxduhgr0e  29510  vtxduhgrun  29515  vtxduhgrfiun  29516  finsumvtxdg2ssteplem1  29577  upgrewlkle2  29638  upgredginwlk  29668  wlkiswwlks1  29896  wlkiswwlksupgr2  29906  umgrwwlks2on  29986  vdn0conngrumgrv2  30224  eulerpathpr  30268  eulercrct  30270  lfuhgr  35101  loop1cycl  35121  umgr2cycllem  35124  isubgrvtxuhgr  47787  isubgredg  47789  isubgrsubgr  47792  isubgr0uhgr  47796  isuspgrim0lem  47808  isuspgrim0  47809  clnbgrgrimlem  47838  clnbgrgrim  47839  grimedg  47840