Metamath Proof Explorer

Theorem nbcplgr

Description: In a complete graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 3-Nov-2020)

Ref Expression
Hypothesis nbcplgr.v ⊢ V = Vtx ⁡ G
Assertion nbcplgr ⊢ G ∈ ComplGraph ∧ N ∈ V → G NeighbVtx N = V ∖ N

Proof

Step Hyp Ref Expression
1 nbcplgr.v ⊢ V = Vtx ⁡ G
2 1 cplgruvtxb ⊢ G ∈ ComplGraph → G ∈ ComplGraph ↔ UnivVtx ⁡ G = V
3 2 ibi ⊢ G ∈ ComplGraph → UnivVtx ⁡ G = V
4 3 eqcomd ⊢ G ∈ ComplGraph → V = UnivVtx ⁡ G
5 4 eleq2d ⊢ G ∈ ComplGraph → N ∈ V ↔ N ∈ UnivVtx ⁡ G
6 5 biimpa ⊢ G ∈ ComplGraph ∧ N ∈ V → N ∈ UnivVtx ⁡ G
7 1 uvtxnbgrb ⊢ N ∈ V → N ∈ UnivVtx ⁡ G ↔ G NeighbVtx N = V ∖ N
8 7 adantl ⊢ G ∈ ComplGraph ∧ N ∈ V → N ∈ UnivVtx ⁡ G ↔ G NeighbVtx N = V ∖ N
9 6 8 mpbid ⊢ G ∈ ComplGraph ∧ N ∈ V → G NeighbVtx N = V ∖ N