This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi 
 |-  ( 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 )