Theorem uhgrfun 28892

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099   ∖ cdif 3944  ∅c0 4323  𝒫 cpw 4603  {csn 4629  dom cdm 5678  Fun wfun 6542  ‘cfv 6548  Vtxcvtx 28822  iEdgciedg 28823  UHGraphcuhgr 28882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-fv 6556  df-uhgr 28884

This theorem is referenced by:  lpvtx  28894  upgrle2  28931  uhgredgiedgb  28952  uhgriedg0edg0  28953  uhgrvtxedgiedgb  28962  edglnl  28969  numedglnl  28970  uhgr2edg  29034  ushgredgedg  29055  ushgredgedgloop  29057  0uhgrsubgr  29105  uhgrsubgrself  29106  subgruhgrfun  29108  subgruhgredgd  29110  subumgredg2  29111  subupgr  29113  uhgrspansubgrlem  29116  uhgrspansubgr  29117  uhgrspan1  29129  upgrreslem  29130  umgrreslem  29131  upgrres  29132  umgrres  29133  vtxduhgr0e  29305  vtxduhgrun  29310  vtxduhgrfiun  29311  finsumvtxdg2ssteplem1  29372  upgrewlkle2  29433  upgredginwlk  29463  wlkiswwlks1  29691  wlkiswwlksupgr2  29701  umgrwwlks2on  29781  vdn0conngrumgrv2  30019  eulerpathpr  30063  eulercrct  30065  lfuhgr  34727  loop1cycl  34747  umgr2cycllem  34750  isuspgrim0lem  47169  isuspgrim0  47170