Metamath Proof Explorer


Theorem cusgruvtxb

Description: A simple graph is complete iff the set of vertices is the set of universal vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by Alexander van der Vekens, 18-Jan-2018) (Revised by AV, 1-Nov-2020)

Ref Expression
Hypothesis iscusgrvtx.v
|- V = ( Vtx ` G )
Assertion cusgruvtxb
|- ( G e. USGraph -> ( G e. ComplUSGraph <-> ( UnivVtx ` G ) = V ) )

Proof

Step Hyp Ref Expression
1 iscusgrvtx.v
 |-  V = ( Vtx ` G )
2 iscusgr
 |-  ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )
3 ibar
 |-  ( G e. USGraph -> ( G e. ComplGraph <-> ( G e. USGraph /\ G e. ComplGraph ) ) )
4 1 cplgruvtxb
 |-  ( G e. USGraph -> ( G e. ComplGraph <-> ( UnivVtx ` G ) = V ) )
5 3 4 bitr3d
 |-  ( G e. USGraph -> ( ( G e. USGraph /\ G e. ComplGraph ) <-> ( UnivVtx ` G ) = V ) )
6 2 5 syl5bb
 |-  ( G e. USGraph -> ( G e. ComplUSGraph <-> ( UnivVtx ` G ) = V ) )