Theorem uhgrfun 29000

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ∖ cdif 3914  ∅c0 4299  𝒫 cpw 4566  {csn 4592  dom cdm 5641  Fun wfun 6508  ‘cfv 6514  Vtxcvtx 28930  iEdgciedg 28931  UHGraphcuhgr 28990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-uhgr 28992

This theorem is referenced by:  lpvtx  29002  upgrle2  29039  uhgredgiedgb  29060  uhgriedg0edg0  29061  uhgrvtxedgiedgb  29070  edglnl  29077  numedglnl  29078  uhgr2edg  29142  ushgredgedg  29163  ushgredgedgloop  29165  0uhgrsubgr  29213  uhgrsubgrself  29214  subgruhgrfun  29216  subgruhgredgd  29218  subumgredg2  29219  subupgr  29221  uhgrspansubgrlem  29224  uhgrspansubgr  29225  uhgrspan1  29237  upgrreslem  29238  umgrreslem  29239  upgrres  29240  umgrres  29241  vtxduhgr0e  29413  vtxduhgrun  29418  vtxduhgrfiun  29419  finsumvtxdg2ssteplem1  29480  upgrewlkle2  29541  upgredginwlk  29571  wlkiswwlks1  29804  wlkiswwlksupgr2  29814  umgrwwlks2on  29894  vdn0conngrumgrv2  30132  eulerpathpr  30176  eulercrct  30178  lfuhgr  35112  loop1cycl  35131  umgr2cycllem  35134  isubgrvtxuhgr  47868  isubgredg  47870  isubgrsubgr  47873  isubgr0uhgr  47877  uhgrimedgi  47894  isuspgrim0lem  47897  isuspgrim0  47898  upgrimwlklem2  47902  upgrimwlklem3  47903  upgrimtrlslem1  47908  clnbgrgrimlem  47937  clnbgrgrim  47938  grimedg  47939