| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > upgruhgr | Structured version Visualization version GIF version | ||
| Description: An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 10-Oct-2020.) |
| Ref | Expression |
|---|---|
| upgruhgr | ⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2737 | . . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺) | |
| 2 | eqid 2737 | . . . 4 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺) | |
| 3 | 1, 2 | upgrf 29175 | . . 3 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) |
| 4 | ssrab2 4034 | . . 3 ⊢ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}) | |
| 5 | fss 6686 | . . 3 ⊢ (((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∧ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅})) | |
| 6 | 3, 4, 5 | sylancl 587 | . 2 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅})) |
| 7 | 1, 2 | isuhgr 29149 | . 2 ⊢ (𝐺 ∈ UPGraph → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))) |
| 8 | 6, 7 | mpbird 257 | 1 ⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2114 {crab 3401 ∖ cdif 3900 ⊆ wss 3903 ∅c0 4287 𝒫 cpw 4556 {csn 4582 class class class wbr 5100 dom cdm 5632 ⟶wf 6496 ‘cfv 6500 ≤ cle 11179 2c2 12212 ♯chash 14265 Vtxcvtx 29085 iEdgciedg 29086 UHGraphcuhgr 29145 UPGraphcupgr 29169 |
| 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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-nul 5253 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-ne 2934 df-rab 3402 df-v 3444 df-sbc 3743 df-dif 3906 df-un 3908 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-fv 6508 df-uhgr 29147 df-upgr 29171 |
| This theorem is referenced by: umgruhgr 29193 upgrle2 29194 edglnl 29232 numedglnl 29233 uspgruhgr 29273 usgruhgr 29275 subupgr 29376 upgrspan 29382 upgrreslem 29393 upgrres 29395 finsumvtxdg2ssteplem1 29635 finsumvtxdg2size 29640 upgrewlkle2 29696 upgredginwlk 29725 wlkiswwlks1 29956 wlkiswwlksupgr2 29966 eulerpathpr 30331 eulercrct 30333 upgracycumgr 35373 isubgrupgr 48234 |
| Copyright terms: Public domain | W3C validator |