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 2738 | . . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺) | |
2 | eqid 2738 | . . . 4 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺) | |
3 | 1, 2 | upgrf 27023 | . . 3 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) |
4 | ssrab2 3967 | . . 3 ⊢ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}) | |
5 | fss 6515 | . . 3 ⊢ (((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∧ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅})) | |
6 | 3, 4, 5 | sylancl 589 | . 2 ⊢ (𝐺 ∈ UPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅})) |
7 | 1, 2 | isuhgr 26997 | . 2 ⊢ (𝐺 ∈ UPGraph → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))) |
8 | 6, 7 | mpbird 260 | 1 ⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2113 {crab 3057 ∖ cdif 3838 ⊆ wss 3841 ∅c0 4209 𝒫 cpw 4485 {csn 4513 class class class wbr 5027 dom cdm 5519 ⟶wf 6329 ‘cfv 6333 ≤ cle 10747 2c2 11764 ♯chash 13775 Vtxcvtx 26933 iEdgciedg 26934 UHGraphcuhgr 26993 UPGraphcupgr 27017 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-nul 5171 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-sbc 3680 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-pw 4487 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-fv 6341 df-uhgr 26995 df-upgr 27019 |
This theorem is referenced by: umgruhgr 27041 upgrle2 27042 edglnl 27080 numedglnl 27081 usgruhgr 27120 subupgr 27221 upgrspan 27227 upgrreslem 27238 upgrres 27240 finsumvtxdg2ssteplem1 27479 finsumvtxdg2size 27484 upgrewlkle2 27540 upgredginwlk 27569 wlkiswwlks1 27797 wlkiswwlksupgr2 27807 eulerpathpr 28169 eulercrct 28171 upgracycumgr 32678 isomuspgrlem2c 44800 |
Copyright terms: Public domain | W3C validator |