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 )