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