Theorem uhgrfun 29160

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ∖ cdif 3887  ∅c0 4268  𝒫 cpw 4536  {csn 4562  dom cdm 5625  Fun wfun 6486  ‘cfv 6492  Vtxcvtx 29090  iEdgciedg 29091  UHGraphcuhgr 29150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-uhgr 29152

This theorem is referenced by:  lpvtx  29162  upgrle2  29199  uhgredgiedgb  29220  uhgriedg0edg0  29221  uhgrvtxedgiedgb  29230  edglnl  29237  numedglnl  29238  uhgr2edg  29302  ushgredgedg  29323  ushgredgedgloop  29325  0uhgrsubgr  29373  uhgrsubgrself  29374  subgruhgrfun  29376  subgruhgredgd  29378  subumgredg2  29379  subupgr  29381  uhgrspansubgrlem  29384  uhgrspansubgr  29385  uhgrspan1  29397  upgrreslem  29398  umgrreslem  29399  upgrres  29400  umgrres  29401  vtxduhgr0e  29572  vtxduhgrun  29577  vtxduhgrfiun  29578  finsumvtxdg2ssteplem1  29639  upgrewlkle2  29700  upgredginwlk  29729  wlkiswwlks1  29960  wlkiswwlksupgr2  29970  usgrwwlks2on  30051  umgrwwlks2on  30052  vdn0conngrumgrv2  30291  eulerpathpr  30335  eulercrct  30337  lfuhgr  35353  loop1cycl  35372  umgr2cycllem  35375  isubgrvtxuhgr  48362  isubgredg  48364  isubgrsubgr  48367  isubgr0uhgr  48371  uhgrimedgi  48388  isuspgrim0lem  48391  isuspgrim0  48392  upgrimwlklem2  48396  upgrimwlklem3  48397  upgrimtrlslem1  48402  clnbgrgrimlem  48431  clnbgrgrim  48432  grimedg  48433