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 USGraph G ComplUSGraph UnivVtx G = V

Proof

Step Hyp Ref Expression
1 iscusgrvtx.v V = Vtx G
2 iscusgr G ComplUSGraph G USGraph G ComplGraph
3 ibar G USGraph G ComplGraph G USGraph G ComplGraph
4 1 cplgruvtxb G USGraph G ComplGraph UnivVtx G = V
5 3 4 bitr3d G USGraph G USGraph G ComplGraph UnivVtx G = V
6 2 5 syl5bb G USGraph G ComplUSGraph UnivVtx G = V