Metamath Proof Explorer

Theorem iscusgrvtx

Description: A simple graph is complete iff all vertices are uniuversal. (Contributed by AV, 1-Nov-2020)

Ref Expression
Hypothesis iscusgrvtx.v ⊢V=Vtx⁡G
Assertion iscusgrvtx ⊢G∈ComplUSGraph↔G∈USGraph∧∀v∈Vv∈UnivVtx⁡G

Proof

Step Hyp Ref Expression
1 iscusgrvtx.v ⊢V=Vtx⁡G
2 iscusgr ⊢G∈ComplUSGraph↔G∈USGraph∧G∈ComplGraph
3 1 iscplgr ⊢G∈USGraph→G∈ComplGraph↔∀v∈Vv∈UnivVtx⁡G
4 3 pm5.32i ⊢G∈USGraph∧G∈ComplGraph↔G∈USGraph∧∀v∈Vv∈UnivVtx⁡G
5 2 4 bitri ⊢G∈ComplUSGraph↔G∈USGraph∧∀v∈Vv∈UnivVtx⁡G