![]() |
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 2731 | . . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺) | |
2 | eqid 2731 | . . . 4 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺) | |
3 | 1, 2 | upgrf 28614 | . . 3 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) |
4 | ssrab2 4077 | . . 3 ⊢ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}) | |
5 | fss 6734 | . . 3 ⊢ (((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∧ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅})) | |
6 | 3, 4, 5 | sylancl 585 | . 2 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅})) |
7 | 1, 2 | isuhgr 28588 | . 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 2105 {crab 3431 ∖ cdif 3945 ⊆ wss 3948 ∅c0 4322 𝒫 cpw 4602 {csn 4628 class class class wbr 5148 dom cdm 5676 ⟶wf 6539 ‘cfv 6543 ≤ cle 11254 2c2 12272 ♯chash 14295 Vtxcvtx 28524 iEdgciedg 28525 UHGraphcuhgr 28584 UPGraphcupgr 28608 |
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 2702 ax-nul 5306 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-ne 2940 df-rab 3432 df-v 3475 df-sbc 3778 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-fv 6551 df-uhgr 28586 df-upgr 28610 |
This theorem is referenced by: umgruhgr 28632 upgrle2 28633 edglnl 28671 numedglnl 28672 usgruhgr 28711 subupgr 28812 upgrspan 28818 upgrreslem 28829 upgrres 28831 finsumvtxdg2ssteplem1 29070 finsumvtxdg2size 29075 upgrewlkle2 29131 upgredginwlk 29161 wlkiswwlks1 29389 wlkiswwlksupgr2 29399 eulerpathpr 29761 eulercrct 29763 upgracycumgr 34443 isomuspgrlem2c 46797 |
Copyright terms: Public domain | W3C validator |