Metamath Proof Explorer

Theorem cusgrop

Description: A complete simple graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020)

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

Proof

Step Hyp Ref Expression
1 usgrop 
 |-  ( G e. USGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. USGraph )
2 cplgrop 
 |-  ( G e. ComplGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. ComplGraph )
3 1 2 anim12i 
 |-  ( ( G e. USGraph /\ G e. ComplGraph ) -> ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. USGraph /\ <. ( Vtx ` G ) , ( iEdg ` G ) >. e. ComplGraph ) )
4 iscusgr 
 |-  ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )
5 iscusgr 
 |-  ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. ComplUSGraph <-> ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. USGraph /\ <. ( Vtx ` G ) , ( iEdg ` G ) >. e. ComplGraph ) )
6 3 4 5 3imtr4i 
 |-  ( G e. ComplUSGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. ComplUSGraph )