Metamath Proof Explorer

Theorem nb3gr2nb

Description: If the neighbors of two vertices in a graph with three elements are an unordered pair of the other vertices, the neighbors of all three vertices are an unordered pair of the other vertices. (Contributed by Alexander van der Vekens, 18-Oct-2017) (Revised by AV, 28-Oct-2020)

Ref Expression
Assertion nb3gr2nb ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → G NeighbVtx A = B C ∧ G NeighbVtx B = A C ↔ G NeighbVtx A = B C ∧ G NeighbVtx B = A C ∧ G NeighbVtx C = A B

Proof

Step Hyp Ref Expression
1 prcom ⊢ A C = C A
2 1 eleq1i ⊢ A C ∈ Edg ⁡ G ↔ C A ∈ Edg ⁡ G
3 2 biimpi ⊢ A C ∈ Edg ⁡ G → C A ∈ Edg ⁡ G
4 3 adantl ⊢ A B ∈ Edg ⁡ G ∧ A C ∈ Edg ⁡ G → C A ∈ Edg ⁡ G
5 prcom ⊢ B C = C B
6 5 eleq1i ⊢ B C ∈ Edg ⁡ G ↔ C B ∈ Edg ⁡ G
7 6 biimpi ⊢ B C ∈ Edg ⁡ G → C B ∈ Edg ⁡ G
8 7 adantl ⊢ B A ∈ Edg ⁡ G ∧ B C ∈ Edg ⁡ G → C B ∈ Edg ⁡ G
9 4 8 anim12i ⊢ A B ∈ Edg ⁡ G ∧ A C ∈ Edg ⁡ G ∧ B A ∈ Edg ⁡ G ∧ B C ∈ Edg ⁡ G → C A ∈ Edg ⁡ G ∧ C B ∈ Edg ⁡ G
10 9 a1i ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → A B ∈ Edg ⁡ G ∧ A C ∈ Edg ⁡ G ∧ B A ∈ Edg ⁡ G ∧ B C ∈ Edg ⁡ G → C A ∈ Edg ⁡ G ∧ C B ∈ Edg ⁡ G
11 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
12 eqid ⊢ Edg ⁡ G = Edg ⁡ G
13 simprr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → G ∈ USGraph
14 simprl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → Vtx ⁡ G = A B C
15 simpl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → A ∈ X ∧ B ∈ Y ∧ C ∈ Z
16 11 12 13 14 15 nb3grprlem1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → G NeighbVtx A = B C ↔ A B ∈ Edg ⁡ G ∧ A C ∈ Edg ⁡ G
17 3ancoma ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ↔ B ∈ Y ∧ A ∈ X ∧ C ∈ Z
18 17 biimpi ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → B ∈ Y ∧ A ∈ X ∧ C ∈ Z
19 tpcoma ⊢ A B C = B A C
20 19 eqeq2i ⊢ Vtx ⁡ G = A B C ↔ Vtx ⁡ G = B A C
21 20 biimpi ⊢ Vtx ⁡ G = A B C → Vtx ⁡ G = B A C
22 21 anim1i ⊢ Vtx ⁡ G = A B C ∧ G ∈ USGraph → Vtx ⁡ G = B A C ∧ G ∈ USGraph
23 simprr ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ Vtx ⁡ G = B A C ∧ G ∈ USGraph → G ∈ USGraph
24 simprl ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ Vtx ⁡ G = B A C ∧ G ∈ USGraph → Vtx ⁡ G = B A C
25 simpl ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ Vtx ⁡ G = B A C ∧ G ∈ USGraph → B ∈ Y ∧ A ∈ X ∧ C ∈ Z
26 11 12 23 24 25 nb3grprlem1 ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ Vtx ⁡ G = B A C ∧ G ∈ USGraph → G NeighbVtx B = A C ↔ B A ∈ Edg ⁡ G ∧ B C ∈ Edg ⁡ G
27 18 22 26 syl2an ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → G NeighbVtx B = A C ↔ B A ∈ Edg ⁡ G ∧ B C ∈ Edg ⁡ G
28 16 27 anbi12d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → G NeighbVtx A = B C ∧ G NeighbVtx B = A C ↔ A B ∈ Edg ⁡ G ∧ A C ∈ Edg ⁡ G ∧ B A ∈ Edg ⁡ G ∧ B C ∈ Edg ⁡ G
29 3anrot ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z
30 29 biimpri ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → C ∈ Z ∧ A ∈ X ∧ B ∈ Y
31 tprot ⊢ C A B = A B C
32 31 eqcomi ⊢ A B C = C A B
33 32 eqeq2i ⊢ Vtx ⁡ G = A B C ↔ Vtx ⁡ G = C A B
34 33 anbi1i ⊢ Vtx ⁡ G = A B C ∧ G ∈ USGraph ↔ Vtx ⁡ G = C A B ∧ G ∈ USGraph
35 34 biimpi ⊢ Vtx ⁡ G = A B C ∧ G ∈ USGraph → Vtx ⁡ G = C A B ∧ G ∈ USGraph
36 simprr ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ Vtx ⁡ G = C A B ∧ G ∈ USGraph → G ∈ USGraph
37 simprl ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ Vtx ⁡ G = C A B ∧ G ∈ USGraph → Vtx ⁡ G = C A B
38 simpl ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ Vtx ⁡ G = C A B ∧ G ∈ USGraph → C ∈ Z ∧ A ∈ X ∧ B ∈ Y
39 11 12 36 37 38 nb3grprlem1 ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ Vtx ⁡ G = C A B ∧ G ∈ USGraph → G NeighbVtx C = A B ↔ C A ∈ Edg ⁡ G ∧ C B ∈ Edg ⁡ G
40 30 35 39 syl2an ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → G NeighbVtx C = A B ↔ C A ∈ Edg ⁡ G ∧ C B ∈ Edg ⁡ G
41 10 28 40 3imtr4d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → G NeighbVtx A = B C ∧ G NeighbVtx B = A C → G NeighbVtx C = A B
42 41 pm4.71d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → G NeighbVtx A = B C ∧ G NeighbVtx B = A C ↔ G NeighbVtx A = B C ∧ G NeighbVtx B = A C ∧ G NeighbVtx C = A B
43 df-3an ⊢ G NeighbVtx A = B C ∧ G NeighbVtx B = A C ∧ G NeighbVtx C = A B ↔ G NeighbVtx A = B C ∧ G NeighbVtx B = A C ∧ G NeighbVtx C = A B
44 42 43 bitr4di ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → G NeighbVtx A = B C ∧ G NeighbVtx B = A C ↔ G NeighbVtx A = B C ∧ G NeighbVtx B = A C ∧ G NeighbVtx C = A B