Metamath Proof Explorer

Theorem cusgr3vnbpr

Description: The neighbors of a vertex in a simple graph with three elements are unordered pairs of the other vertices if and only if the graph is complete. (Contributed by Alexander van der Vekens, 18-Oct-2017) (Revised by AV, 5-Nov-2020)

Ref Expression
Hypotheses cplgr3v.e ⊢ E = Edg ⁡ G
cplgr3v.t ⊢ Vtx ⁡ G = A B C
cplgr3v.v ⊢ V = Vtx ⁡ G
Assertion cusgr3vnbpr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ G ∈ USGraph ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → G ∈ ComplGraph ↔ ∀ x ∈ V ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z

Proof

Step Hyp Ref Expression
1 cplgr3v.e ⊢ E = Edg ⁡ G
2 cplgr3v.t ⊢ Vtx ⁡ G = A B C
3 cplgr3v.v ⊢ V = Vtx ⁡ G
4 usgrupgr ⊢ G ∈ USGraph → G ∈ UPGraph
5 1 2 cplgr3v ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ G ∈ UPGraph ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → G ∈ ComplGraph ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
6 4 5 syl3an2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ G ∈ USGraph ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → G ∈ ComplGraph ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
7 simp2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ G ∈ USGraph ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → G ∈ USGraph
8 3 2 eqtri ⊢ V = A B C
9 8 a1i ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ G ∈ USGraph ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → V = A B C
10 simp1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ G ∈ USGraph ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → A ∈ X ∧ B ∈ Y ∧ C ∈ Z
11 simp3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ G ∈ USGraph ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → A ≠ B ∧ A ≠ C ∧ B ≠ C
12 3 1 7 9 10 11 nb3grpr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ G ∈ USGraph ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ ∀ x ∈ V ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z
13 6 12 bitrd ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ G ∈ USGraph ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → G ∈ ComplGraph ↔ ∀ x ∈ V ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z