Theorem uhgrfun 26300

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

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157   ∖ cdif 3767  ∅c0 4116  𝒫 cpw 4350  {csn 4369  dom cdm 5313  Fun wfun 6096  ‘cfv 6102  Vtxcvtx 26230  iEdgciedg 26231  UHGraphcuhgr 26290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-nul 4984

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2592  df-eu 2610  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3388  df-sbc 3635  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-pw 4352  df-sn 4370  df-pr 4372  df-op 4376  df-uni 4630  df-br 4845  df-opab 4907  df-rel 5320  df-cnv 5321  df-co 5322  df-dm 5323  df-rn 5324  df-iota 6065  df-fun 6104  df-fn 6105  df-f 6106  df-fv 6110  df-uhgr 26292

This theorem is referenced by:  lpvtx  26302  upgrle2  26339  uhgredgiedgb  26360  uhgriedg0edg0  26361  uhgrvtxedgiedgb  26370  uhgrvtxedgiedgbOLD  26371  edglnl  26378  numedglnl  26379  uhgr2edg  26440  ushgredgedg  26461  ushgredgedgloop  26463  ushgredgedgloopOLD  26464  0uhgrsubgr  26512  uhgrsubgrself  26513  subgruhgrfun  26515  subgruhgredgd  26517  subumgredg2  26518  subupgr  26520  uhgrspansubgrlem  26523  uhgrspansubgr  26524  uhgrspan1  26536  upgrreslem  26537  umgrreslem  26538  upgrres  26539  umgrres  26540  vtxduhgr0e  26727  vtxduhgrun  26732  vtxduhgrfiun  26733  finsumvtxdg2ssteplem1  26794  upgrewlkle2  26855  upgredginwlk  26884  wlkiswwlks1  27123  wlkiswwlksupgr2  27133  umgrwwlks2on  27246  vdn0conngrumgrv2  27539  eulerpathpr  27584  eulercrct  27586