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

Metamath Proof Explorer

Theorem umgrupgr

Description: An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020)

Ref Expression
Assertion umgrupgr 
|- ( G e. UMGraph -> G e. UPGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 isumgr 
 |-  ( G e. UMGraph -> ( G e. UMGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } ) )
4 id 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } )
5 2re 
 |-  2 e. RR
6 5 leidi 
 |-  2 <_ 2
7 6 a1i 
 |-  ( ( # ` x ) = 2 -> 2 <_ 2 )
8 breq1 
 |-  ( ( # ` x ) = 2 -> ( ( # ` x ) <_ 2 <-> 2 <_ 2 ) )
9 7 8 mpbird 
 |-  ( ( # ` x ) = 2 -> ( # ` x ) <_ 2 )
10 9 a1i 
 |-  ( x e. ( ~P ( Vtx ` G ) \ { (/) } ) -> ( ( # ` x ) = 2 -> ( # ` x ) <_ 2 ) )
11 10 ss2rabi 
 |-  { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 }
12 11 a1i 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } -> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
13 4 12 fssd 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
14 3 13 biimtrdi 
 |-  ( G e. UMGraph -> ( G e. UMGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
15 14 pm2.43i 
 |-  ( G e. UMGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
16 1 2 isupgr 
 |-  ( G e. UMGraph -> ( G e. UPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
17 15 16 mpbird 
 |-  ( G e. UMGraph -> G e. UPGraph )