Theorem uhgrfun 29139

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ∖ cdif 3898  ∅c0 4285  𝒫 cpw 4554  {csn 4580  dom cdm 5624  Fun wfun 6486  ‘cfv 6492  Vtxcvtx 29069  iEdgciedg 29070  UHGraphcuhgr 29129

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-uhgr 29131

This theorem is referenced by:  lpvtx  29141  upgrle2  29178  uhgredgiedgb  29199  uhgriedg0edg0  29200  uhgrvtxedgiedgb  29209  edglnl  29216  numedglnl  29217  uhgr2edg  29281  ushgredgedg  29302  ushgredgedgloop  29304  0uhgrsubgr  29352  uhgrsubgrself  29353  subgruhgrfun  29355  subgruhgredgd  29357  subumgredg2  29358  subupgr  29360  uhgrspansubgrlem  29363  uhgrspansubgr  29364  uhgrspan1  29376  upgrreslem  29377  umgrreslem  29378  upgrres  29379  umgrres  29380  vtxduhgr0e  29552  vtxduhgrun  29557  vtxduhgrfiun  29558  finsumvtxdg2ssteplem1  29619  upgrewlkle2  29680  upgredginwlk  29709  wlkiswwlks1  29940  wlkiswwlksupgr2  29950  usgrwwlks2on  30031  umgrwwlks2on  30032  vdn0conngrumgrv2  30271  eulerpathpr  30315  eulercrct  30317  lfuhgr  35312  loop1cycl  35331  umgr2cycllem  35334  isubgrvtxuhgr  48106  isubgredg  48108  isubgrsubgr  48111  isubgr0uhgr  48115  uhgrimedgi  48132  isuspgrim0lem  48135  isuspgrim0  48136  upgrimwlklem2  48140  upgrimwlklem3  48141  upgrimtrlslem1  48146  clnbgrgrimlem  48175  clnbgrgrim  48176  grimedg  48177