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 ∈ V v ∈ 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 ∈ V v ∈ UnivVtx ⁡ G
4 3 pm5.32i ⊢ G ∈ USGraph ∧ G ∈ ComplGraph ↔ G ∈ USGraph ∧ ∀ v ∈ V v ∈ UnivVtx ⁡ G
5 2 4 bitri ⊢ G ∈ ComplUSGraph ↔ G ∈ USGraph ∧ ∀ v ∈ V v ∈ UnivVtx ⁡ G