Theorem uhgrfun 28993

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ∖ cdif 3911  ∅c0 4296  𝒫 cpw 4563  {csn 4589  dom cdm 5638  Fun wfun 6505  ‘cfv 6511  Vtxcvtx 28923  iEdgciedg 28924  UHGraphcuhgr 28983

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 2701  ax-nul 5261

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-uhgr 28985

This theorem is referenced by:  lpvtx  28995  upgrle2  29032  uhgredgiedgb  29053  uhgriedg0edg0  29054  uhgrvtxedgiedgb  29063  edglnl  29070  numedglnl  29071  uhgr2edg  29135  ushgredgedg  29156  ushgredgedgloop  29158  0uhgrsubgr  29206  uhgrsubgrself  29207  subgruhgrfun  29209  subgruhgredgd  29211  subumgredg2  29212  subupgr  29214  uhgrspansubgrlem  29217  uhgrspansubgr  29218  uhgrspan1  29230  upgrreslem  29231  umgrreslem  29232  upgrres  29233  umgrres  29234  vtxduhgr0e  29406  vtxduhgrun  29411  vtxduhgrfiun  29412  finsumvtxdg2ssteplem1  29473  upgrewlkle2  29534  upgredginwlk  29564  wlkiswwlks1  29797  wlkiswwlksupgr2  29807  umgrwwlks2on  29887  vdn0conngrumgrv2  30125  eulerpathpr  30169  eulercrct  30171  lfuhgr  35105  loop1cycl  35124  umgr2cycllem  35127  isubgrvtxuhgr  47864  isubgredg  47866  isubgrsubgr  47869  isubgr0uhgr  47873  uhgrimedgi  47890  isuspgrim0lem  47893  isuspgrim0  47894  upgrimwlklem2  47898  upgrimwlklem3  47899  upgrimtrlslem1  47904  clnbgrgrimlem  47933  clnbgrgrim  47934  grimedg  47935