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 bilani ⊢ A B ∈ Edg ⁡ G ∧ A C ∈ Edg ⁡ G → C A ∈ Edg ⁡ G
4 prcom ⊢ B C = C B
5 4 eleq1i ⊢ B C ∈ Edg ⁡ G ↔ C B ∈ Edg ⁡ G
6 5 bilani ⊢ B A ∈ Edg ⁡ G ∧ B C ∈ Edg ⁡ G → C B ∈ Edg ⁡ G
7 3 6 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
8 7 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
9 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
10 eqid ⊢ Edg ⁡ G = Edg ⁡ G
11 simprr ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → G ∈ USGraph
12 simprl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → Vtx ⁡ G = A B C
13 simpl ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ Vtx ⁡ G = A B C ∧ G ∈ USGraph → A ∈ X ∧ B ∈ Y ∧ C ∈ Z
14 9 10 11 12 13 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
15 3ancoma ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ↔ B ∈ Y ∧ A ∈ X ∧ C ∈ Z
16 15 biimpi ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → B ∈ Y ∧ A ∈ X ∧ C ∈ Z
17 tpcoma ⊢ A B C = B A C
18 17 eqeq2i ⊢ Vtx ⁡ G = A B C ↔ Vtx ⁡ G = B A C
19 18 biimpi ⊢ Vtx ⁡ G = A B C → Vtx ⁡ G = B A C
20 19 anim1i ⊢ Vtx ⁡ G = A B C ∧ G ∈ USGraph → Vtx ⁡ G = B A C ∧ G ∈ USGraph
21 simprr ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ Vtx ⁡ G = B A C ∧ G ∈ USGraph → G ∈ USGraph
22 simprl ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ Vtx ⁡ G = B A C ∧ G ∈ USGraph → Vtx ⁡ G = B A C
23 simpl ⊢ B ∈ Y ∧ A ∈ X ∧ C ∈ Z ∧ Vtx ⁡ G = B A C ∧ G ∈ USGraph → B ∈ Y ∧ A ∈ X ∧ C ∈ Z
24 9 10 21 22 23 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
25 16 20 24 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
26 14 25 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
27 3anrot ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z
28 27 biimpri ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → C ∈ Z ∧ A ∈ X ∧ B ∈ Y
29 tprot ⊢ C A B = A B C
30 29 eqcomi ⊢ A B C = C A B
31 30 eqeq2i ⊢ Vtx ⁡ G = A B C ↔ Vtx ⁡ G = C A B
32 31 anbi1i ⊢ Vtx ⁡ G = A B C ∧ G ∈ USGraph ↔ Vtx ⁡ G = C A B ∧ G ∈ USGraph
33 32 biimpi ⊢ Vtx ⁡ G = A B C ∧ G ∈ USGraph → Vtx ⁡ G = C A B ∧ G ∈ USGraph
34 simprr ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ Vtx ⁡ G = C A B ∧ G ∈ USGraph → G ∈ USGraph
35 simprl ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ Vtx ⁡ G = C A B ∧ G ∈ USGraph → Vtx ⁡ G = C A B
36 simpl ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ∧ Vtx ⁡ G = C A B ∧ G ∈ USGraph → C ∈ Z ∧ A ∈ X ∧ B ∈ Y
37 9 10 34 35 36 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
38 28 33 37 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
39 8 26 38 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
40 39 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
41 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
42 40 41 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