Theorem usgruspgr

Description: A simple graph is a simple pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 15-Oct-2020)

	Ref	Expression
Assertion	usgruspgr	|- ( G e. USGraph -> G e. USPGraph )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
2		eqid	|- ( iEdg ` G ) = ( iEdg ` G )
3	1 2	isusgr	|- ( G e. USGraph -> ( G e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } ) )
4		2re	|- 2 e. RR
5	4	eqlei2	|- ( ( # ` x ) = 2 -> ( # ` x ) <_ 2 )
6	5	a1i	|- ( x e. ( ~P ( Vtx ` G ) \ { (/) } ) -> ( ( # ` x ) = 2 -> ( # ` x ) <_ 2 ) )
7	6	ss2rabi	|- { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 }
8		f1ss	|- ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } /\ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
9	7 8	mpan2	|- ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
10	3 9	syl6bi	|- ( G e. USGraph -> ( G e. USGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
11	1 2	isuspgr	|- ( G e. USGraph -> ( G e. USPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
12	10 11	sylibrd	|- ( G e. USGraph -> ( G e. USGraph -> G e. USPGraph ) )
13	12	pm2.43i	|- ( G e. USGraph -> G e. USPGraph )