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 e. USPGraph -> G e. UPGraph )`

Proof

Step Hyp Ref Expression
1 eqid
` |-  ( Vtx ` G ) = ( Vtx ` G )`
2 eqid
` |-  ( iEdg ` G ) = ( iEdg ` G )`
3 1 2 isuspgr
` |-  ( G e. USPGraph -> ( G e. USPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )`
4 f1f
` |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )`
5 3 4 syl6bi
` |-  ( G e. USPGraph -> ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )`
6 1 2 isupgr
` |-  ( G e. USPGraph -> ( G e. UPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )`
7 5 6 sylibrd
` |-  ( G e. USPGraph -> ( G e. USPGraph -> G e. UPGraph ) )`
8 7 pm2.43i
` |-  ( G e. USPGraph -> G e. UPGraph )`