# Metamath Proof Explorer

## Theorem uspgrupgr

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
Assertion uspgrupgr ${⊢}{G}\in \mathrm{USHGraph}\to {G}\in \mathrm{UPGraph}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
2 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
3 1 2 isuspgr ${⊢}{G}\in \mathrm{USHGraph}\to \left({G}\in \mathrm{USHGraph}↔\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}\right)$
4 f1f ${⊢}\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}\to \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$
5 3 4 syl6bi ${⊢}{G}\in \mathrm{USHGraph}\to \left({G}\in \mathrm{USHGraph}\to \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}\right)$
6 1 2 isupgr ${⊢}{G}\in \mathrm{USHGraph}\to \left({G}\in \mathrm{UPGraph}↔\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}\right)$
7 5 6 sylibrd ${⊢}{G}\in \mathrm{USHGraph}\to \left({G}\in \mathrm{USHGraph}\to {G}\in \mathrm{UPGraph}\right)$
8 7 pm2.43i ${⊢}{G}\in \mathrm{USHGraph}\to {G}\in \mathrm{UPGraph}$