Theorem uhgrfun 29012

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ∖ cdif 3928  ∅c0 4313  𝒫 cpw 4580  {csn 4606  dom cdm 5665  Fun wfun 6535  ‘cfv 6541  Vtxcvtx 28942  iEdgciedg 28943  UHGraphcuhgr 29002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-nul 5286

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-rab 3420  df-v 3465  df-sbc 3771  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-uhgr 29004

This theorem is referenced by:  lpvtx  29014  upgrle2  29051  uhgredgiedgb  29072  uhgriedg0edg0  29073  uhgrvtxedgiedgb  29082  edglnl  29089  numedglnl  29090  uhgr2edg  29154  ushgredgedg  29175  ushgredgedgloop  29177  0uhgrsubgr  29225  uhgrsubgrself  29226  subgruhgrfun  29228  subgruhgredgd  29230  subumgredg2  29231  subupgr  29233  uhgrspansubgrlem  29236  uhgrspansubgr  29237  uhgrspan1  29249  upgrreslem  29250  umgrreslem  29251  upgrres  29252  umgrres  29253  vtxduhgr0e  29425  vtxduhgrun  29430  vtxduhgrfiun  29431  finsumvtxdg2ssteplem1  29492  upgrewlkle2  29553  upgredginwlk  29583  wlkiswwlks1  29816  wlkiswwlksupgr2  29826  umgrwwlks2on  29906  vdn0conngrumgrv2  30144  eulerpathpr  30188  eulercrct  30190  lfuhgr  35098  loop1cycl  35117  umgr2cycllem  35120  isubgrvtxuhgr  47823  isubgredg  47825  isubgrsubgr  47828  isubgr0uhgr  47832  isuspgrim0lem  47844  isuspgrim0  47845  clnbgrgrimlem  47874  clnbgrgrim  47875  grimedg  47876