Metamath Proof Explorer

Theorem uspgrushgr

Description: A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020) (Revised by AV, 15-Oct-2020)

Ref Expression
Assertion uspgrushgr 
|- ( G e. USPGraph -> G e. USHGraph )

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 ssrab2 
 |-  { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } C_ ( ~P ( Vtx ` G ) \ { (/) } )
5 f1ss 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } /\ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } C_ ( ~P ( Vtx ` G ) \ { (/) } ) ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( ~P ( Vtx ` G ) \ { (/) } ) )
6 4 5 mpan2 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( ~P ( Vtx ` G ) \ { (/) } ) )
7 3 6 syl6bi 
 |-  ( G e. USPGraph -> ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( ~P ( Vtx ` G ) \ { (/) } ) ) )
8 1 2 isushgr 
 |-  ( G e. USPGraph -> ( G e. USHGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( ~P ( Vtx ` G ) \ { (/) } ) ) )
9 7 8 sylibrd 
 |-  ( G e. USPGraph -> ( G e. USPGraph -> G e. USHGraph ) )
10 9 pm2.43i 
 |-  ( G e. USPGraph -> G e. USHGraph )