Metamath Proof Explorer

Theorem iscplgrnb

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

Ref Expression
Hypothesis cplgruvtxb.v ⊢ V = Vtx ⁡ G
Assertion iscplgrnb ⊢ G ∈ W → G ∈ ComplGraph ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v

Proof

Step Hyp Ref Expression
1 cplgruvtxb.v ⊢ V = Vtx ⁡ G
2 1 iscplgr ⊢ G ∈ W → G ∈ ComplGraph ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
3 1 uvtxel ⊢ v ∈ UnivVtx ⁡ G ↔ v ∈ V ∧ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
4 3 a1i ⊢ G ∈ W → v ∈ UnivVtx ⁡ G ↔ v ∈ V ∧ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
5 4 baibd ⊢ G ∈ W ∧ v ∈ V → v ∈ UnivVtx ⁡ G ↔ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
6 5 ralbidva ⊢ G ∈ W → ∀ v ∈ V v ∈ UnivVtx ⁡ G ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
7 2 6 bitrd ⊢ G ∈ W → G ∈ ComplGraph ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v