Theorem uhgrfun 25732

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 2610	. . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		uhgrfun.e	. . 3 ⊢ 𝐸 = (iEdg‘𝐺)
3	1, 2	uhgrf 25728	. 2 ⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
4		ffun 5961	. 2 ⊢ (𝐸:dom 𝐸⟶(𝒫 (Vtx‘𝐺) ∖ {∅}) → Fun 𝐸)
5	3, 4	syl 17	1 ⊢ (𝐺 ∈ UHGraph → Fun 𝐸)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977   ∖ cdif 3537  ∅c0 3874  𝒫 cpw 4108  {csn 4125  dom cdm 5038  Fun wfun 5798  ⟶wf 5800  ‘cfv 5804  Vtxcvtx 25673  iEdgciedg 25674   UHGraph cuhgr 25722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-uhgr 25724

This theorem is referenced by:  lpvtx  25734  upgrle2  25771  uhgredgiedgb  25799  uhgriedg0edg0  25801  uhgrvtxedgiedgb  25810  uhgr2edg  40435  ushgredgedga  40456  ushgredgedgaloop  40458  0uhgrsubgr  40503  uhgrsubgrself  40504  subgruhgrfun  40506  subgruhgredgd  40508  subumgredg2  40509  subupgr  40511  uhgrspansubgrlem  40514  uhgrspansubgr  40515  uhgrspan1  40527  vtxduhgr0e  40693  vtxduhgrun  40698  vtxduhgrfiun  40699  upgrewlkle2  40808  upgredginwlk  40840  1wlkiswwlks1  41064  1wlkiswwlksupgr2  41074  umgrwwlks2on  41161  vdn0conngrumgrv2  41363  eulerpathpr  41408  eulercrct  41410