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 bitrid ⊢G∈USGraph→G∈ComplUSGraph↔UnivVtx⁡G=V