Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uhgrfun | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
uhgrfun.e | ⊢ 𝐸 = (iEdg‘𝐺) |
Ref | Expression |
---|---|
uhgrfun | ⊢ (𝐺 ∈ UHGraph → Fun 𝐸) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2736 | . . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺) | |
2 | uhgrfun.e | . . 3 ⊢ 𝐸 = (iEdg‘𝐺) | |
3 | 1, 2 | uhgrf 27721 | . 2 ⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 (Vtx‘𝐺) ∖ {∅})) |
4 | 3 | ffund 6655 | 1 ⊢ (𝐺 ∈ UHGraph → Fun 𝐸) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2105 ∖ cdif 3895 ∅c0 4269 𝒫 cpw 4547 {csn 4573 dom cdm 5620 Fun wfun 6473 ‘cfv 6479 Vtxcvtx 27655 iEdgciedg 27656 UHGraphcuhgr 27715 |
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 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2707 ax-nul 5250 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2941 df-rab 3404 df-v 3443 df-sbc 3728 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-br 5093 df-opab 5155 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-fv 6487 df-uhgr 27717 |
This theorem is referenced by: lpvtx 27727 upgrle2 27764 uhgredgiedgb 27785 uhgriedg0edg0 27786 uhgrvtxedgiedgb 27795 edglnl 27802 numedglnl 27803 uhgr2edg 27864 ushgredgedg 27885 ushgredgedgloop 27887 0uhgrsubgr 27935 uhgrsubgrself 27936 subgruhgrfun 27938 subgruhgredgd 27940 subumgredg2 27941 subupgr 27943 uhgrspansubgrlem 27946 uhgrspansubgr 27947 uhgrspan1 27959 upgrreslem 27960 umgrreslem 27961 upgrres 27962 umgrres 27963 vtxduhgr0e 28134 vtxduhgrun 28139 vtxduhgrfiun 28140 finsumvtxdg2ssteplem1 28201 upgrewlkle2 28262 upgredginwlk 28292 wlkiswwlks1 28520 wlkiswwlksupgr2 28530 umgrwwlks2on 28610 vdn0conngrumgrv2 28848 eulerpathpr 28892 eulercrct 28894 lfuhgr 33378 loop1cycl 33398 umgr2cycllem 33401 |
Copyright terms: Public domain | W3C validator |