![]() |
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 28450 | . . . 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 28382 | . . 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 11251 2c2 12269 ♯chash 14292 Vtxcvtx 28294 iEdgciedg 28295 UPGraphcupgr 28378 USPGraphcuspgr 28446 |
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 28380 df-uspgr 28448 |
This theorem is referenced by: uspgrupgrushgr 28475 usgrupgr 28480 uspgrun 28483 uspgrunop 28484 uspgredg2vtxeu 28515 1loopgrnb0 28797 uspgr2wlkeq 28941 uspgrn2crct 29100 wlkiswwlks2 29167 wlkiswwlks 29168 wlklnwwlkn 29176 clwlkclwwlk 29293 wlk2v2e 29448 isomuspgrlem1 46574 isomuspgrlem2b 46576 isomuspgrlem2c 46577 isomuspgrlem2d 46578 uspgropssxp 46601 uspgrsprf 46603 |
Copyright terms: Public domain | W3C validator |