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

Metamath Proof Explorer

Theorem upgruhgr

Description: An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 10-Oct-2020)

Ref Expression
Assertion upgruhgr 
|- ( G e. UPGraph -> G e. UHGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 upgrf 
 |-  ( G e. UPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
4 ssrab2 
 |-  { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } C_ ( ~P ( Vtx ` G ) \ { (/) } )
5 fss 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } /\ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } C_ ( ~P ( Vtx ` G ) \ { (/) } ) ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) )
6 3 4 5 sylancl 
 |-  ( G e. UPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) )
7 1 2 isuhgr 
 |-  ( G e. UPGraph -> ( G e. UHGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) ) )
8 6 7 mpbird 
 |-  ( G e. UPGraph -> G e. UHGraph )