![]() |
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 2798 | . . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺) | |
2 | uhgrfun.e | . . 3 ⊢ 𝐸 = (iEdg‘𝐺) | |
3 | 1, 2 | uhgrf 26855 | . 2 ⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 (Vtx‘𝐺) ∖ {∅})) |
4 | 3 | ffund 6491 | 1 ⊢ (𝐺 ∈ UHGraph → Fun 𝐸) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 ∖ cdif 3878 ∅c0 4243 𝒫 cpw 4497 {csn 4525 dom cdm 5519 Fun wfun 6318 ‘cfv 6324 Vtxcvtx 26789 iEdgciedg 26790 UHGraphcuhgr 26849 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-nul 5174 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-fv 6332 df-uhgr 26851 |
This theorem is referenced by: lpvtx 26861 upgrle2 26898 uhgredgiedgb 26919 uhgriedg0edg0 26920 uhgrvtxedgiedgb 26929 edglnl 26936 numedglnl 26937 uhgr2edg 26998 ushgredgedg 27019 ushgredgedgloop 27021 0uhgrsubgr 27069 uhgrsubgrself 27070 subgruhgrfun 27072 subgruhgredgd 27074 subumgredg2 27075 subupgr 27077 uhgrspansubgrlem 27080 uhgrspansubgr 27081 uhgrspan1 27093 upgrreslem 27094 umgrreslem 27095 upgrres 27096 umgrres 27097 vtxduhgr0e 27268 vtxduhgrun 27273 vtxduhgrfiun 27274 finsumvtxdg2ssteplem1 27335 upgrewlkle2 27396 upgredginwlk 27425 wlkiswwlks1 27653 wlkiswwlksupgr2 27663 umgrwwlks2on 27743 vdn0conngrumgrv2 27981 eulerpathpr 28025 eulercrct 28027 lfuhgr 32477 loop1cycl 32497 umgr2cycllem 32500 |
Copyright terms: Public domain | W3C validator |