MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uhgrfun Structured version   Visualization version   GIF version

Theorem uhgrfun 27725
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
StepHypRef Expression
1 eqid 2736 . . 3 (Vtx‘𝐺) = (Vtx‘𝐺)
2 uhgrfun.e . . 3 𝐸 = (iEdg‘𝐺)
31, 2uhgrf 27721 . 2 (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
43ffund 6655 1 (𝐺 ∈ UHGraph → Fun 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2105  cdif 3895  c0 4269  𝒫 cpw 4547  {csn 4573  dom cdm 5620  Fun wfun 6473  cfv 6479  Vtxcvtx 27655  iEdgciedg 27656  UHGraphcuhgr 27715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-nul 5250
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-rab 3404  df-v 3443  df-sbc 3728  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-fv 6487  df-uhgr 27717
This theorem is referenced by:  lpvtx  27727  upgrle2  27764  uhgredgiedgb  27785  uhgriedg0edg0  27786  uhgrvtxedgiedgb  27795  edglnl  27802  numedglnl  27803  uhgr2edg  27864  ushgredgedg  27885  ushgredgedgloop  27887  0uhgrsubgr  27935  uhgrsubgrself  27936  subgruhgrfun  27938  subgruhgredgd  27940  subumgredg2  27941  subupgr  27943  uhgrspansubgrlem  27946  uhgrspansubgr  27947  uhgrspan1  27959  upgrreslem  27960  umgrreslem  27961  upgrres  27962  umgrres  27963  vtxduhgr0e  28134  vtxduhgrun  28139  vtxduhgrfiun  28140  finsumvtxdg2ssteplem1  28201  upgrewlkle2  28262  upgredginwlk  28292  wlkiswwlks1  28520  wlkiswwlksupgr2  28530  umgrwwlks2on  28610  vdn0conngrumgrv2  28848  eulerpathpr  28892  eulercrct  28894  lfuhgr  33378  loop1cycl  33398  umgr2cycllem  33401
  Copyright terms: Public domain W3C validator