![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uspgrupgr | Structured version Visualization version GIF version |
Description: A simple pseudograph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.) |
Ref | Expression |
---|---|
uspgrupgr | ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2732 | . . . . 5 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺) | |
2 | eqid 2732 | . . . . 5 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺) | |
3 | 1, 2 | isuspgr 28409 | . . . 4 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})) |
4 | f1f 6787 | . . . 4 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) | |
5 | 3, 4 | syl6bi 252 | . . 3 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})) |
6 | 1, 2 | isupgr 28341 | . . 3 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ UPGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})) |
7 | 5, 6 | sylibrd 258 | . 2 ⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)) |
8 | 7 | pm2.43i 52 | 1 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 {crab 3432 ∖ cdif 3945 ∅c0 4322 𝒫 cpw 4602 {csn 4628 class class class wbr 5148 dom cdm 5676 ⟶wf 6539 –1-1→wf1 6540 ‘cfv 6543 ≤ cle 11248 2c2 12266 ♯chash 14289 Vtxcvtx 28253 iEdgciedg 28254 UPGraphcupgr 28337 USPGraphcuspgr 28405 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-nul 5306 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ne 2941 df-rab 3433 df-v 3476 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-f1 6548 df-fv 6551 df-upgr 28339 df-uspgr 28407 |
This theorem is referenced by: uspgrupgrushgr 28434 usgrupgr 28439 uspgrun 28442 uspgrunop 28443 uspgredg2vtxeu 28474 1loopgrnb0 28756 uspgr2wlkeq 28900 uspgrn2crct 29059 wlkiswwlks2 29126 wlkiswwlks 29127 wlklnwwlkn 29135 clwlkclwwlk 29252 wlk2v2e 29407 isomuspgrlem1 46485 isomuspgrlem2b 46487 isomuspgrlem2c 46488 isomuspgrlem2d 46489 uspgropssxp 46512 uspgrsprf 46514 |
Copyright terms: Public domain | W3C validator |