Metamath Proof Explorer

Theorem usgrop

Description: A simple graph represented by an ordered pair. (Contributed by AV, 23-Oct-2020) (Proof shortened by AV, 30-Nov-2020)

Ref Expression
Assertion usgrop 
|- ( G e. USGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. USGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 usgrfs 
 |-  ( G e. USGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
4 fvex 
 |-  ( Vtx ` G ) e. _V
5 fvex 
 |-  ( iEdg ` G ) e. _V
6 4 5 pm3.2i 
 |-  ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V )
7 isusgrop 
 |-  ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
8 6 7 mp1i 
 |-  ( G e. USGraph -> ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
9 3 8 mpbird 
 |-  ( G e. USGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. USGraph )