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=ABC∧G∈USGraph→GNeighbVtxA=BC∧GNeighbVtxB=AC↔GNeighbVtxA=BC∧GNeighbVtxB=AC∧GNeighbVtxC=AB

Proof

Step Hyp Ref Expression
1 prcom ⊢AC=CA
2 1 eleq1i ⊢AC∈Edg⁡G↔CA∈Edg⁡G
3 2 biimpi ⊢AC∈Edg⁡G→CA∈Edg⁡G
4 3 adantl ⊢AB∈Edg⁡G∧AC∈Edg⁡G→CA∈Edg⁡G
5 prcom ⊢BC=CB
6 5 eleq1i ⊢BC∈Edg⁡G↔CB∈Edg⁡G
7 6 biimpi ⊢BC∈Edg⁡G→CB∈Edg⁡G
8 7 adantl ⊢BA∈Edg⁡G∧BC∈Edg⁡G→CB∈Edg⁡G
9 4 8 anim12i ⊢AB∈Edg⁡G∧AC∈Edg⁡G∧BA∈Edg⁡G∧BC∈Edg⁡G→CA∈Edg⁡G∧CB∈Edg⁡G
10 9 a1i ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→AB∈Edg⁡G∧AC∈Edg⁡G∧BA∈Edg⁡G∧BC∈Edg⁡G→CA∈Edg⁡G∧CB∈Edg⁡G
11 eqid ⊢Vtx⁡G=Vtx⁡G
12 eqid ⊢Edg⁡G=Edg⁡G
13 simprr ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→G∈USGraph
14 simprl ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→Vtx⁡G=ABC
15 simpl ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→A∈X∧B∈Y∧C∈Z
16 11 12 13 14 15 nb3grprlem1 ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→GNeighbVtxA=BC↔AB∈Edg⁡G∧AC∈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 ⊢ABC=BAC
20 19 eqeq2i ⊢Vtx⁡G=ABC↔Vtx⁡G=BAC
21 20 biimpi ⊢Vtx⁡G=ABC→Vtx⁡G=BAC
22 21 anim1i ⊢Vtx⁡G=ABC∧G∈USGraph→Vtx⁡G=BAC∧G∈USGraph
23 simprr ⊢B∈Y∧A∈X∧C∈Z∧Vtx⁡G=BAC∧G∈USGraph→G∈USGraph
24 simprl ⊢B∈Y∧A∈X∧C∈Z∧Vtx⁡G=BAC∧G∈USGraph→Vtx⁡G=BAC
25 simpl ⊢B∈Y∧A∈X∧C∈Z∧Vtx⁡G=BAC∧G∈USGraph→B∈Y∧A∈X∧C∈Z
26 11 12 23 24 25 nb3grprlem1 ⊢B∈Y∧A∈X∧C∈Z∧Vtx⁡G=BAC∧G∈USGraph→GNeighbVtxB=AC↔BA∈Edg⁡G∧BC∈Edg⁡G
27 18 22 26 syl2an ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→GNeighbVtxB=AC↔BA∈Edg⁡G∧BC∈Edg⁡G
28 16 27 anbi12d ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→GNeighbVtxA=BC∧GNeighbVtxB=AC↔AB∈Edg⁡G∧AC∈Edg⁡G∧BA∈Edg⁡G∧BC∈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 ⊢CAB=ABC
32 31 eqcomi ⊢ABC=CAB
33 32 eqeq2i ⊢Vtx⁡G=ABC↔Vtx⁡G=CAB
34 33 anbi1i ⊢Vtx⁡G=ABC∧G∈USGraph↔Vtx⁡G=CAB∧G∈USGraph
35 34 biimpi ⊢Vtx⁡G=ABC∧G∈USGraph→Vtx⁡G=CAB∧G∈USGraph
36 simprr ⊢C∈Z∧A∈X∧B∈Y∧Vtx⁡G=CAB∧G∈USGraph→G∈USGraph
37 simprl ⊢C∈Z∧A∈X∧B∈Y∧Vtx⁡G=CAB∧G∈USGraph→Vtx⁡G=CAB
38 simpl ⊢C∈Z∧A∈X∧B∈Y∧Vtx⁡G=CAB∧G∈USGraph→C∈Z∧A∈X∧B∈Y
39 11 12 36 37 38 nb3grprlem1 ⊢C∈Z∧A∈X∧B∈Y∧Vtx⁡G=CAB∧G∈USGraph→GNeighbVtxC=AB↔CA∈Edg⁡G∧CB∈Edg⁡G
40 30 35 39 syl2an ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→GNeighbVtxC=AB↔CA∈Edg⁡G∧CB∈Edg⁡G
41 10 28 40 3imtr4d ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→GNeighbVtxA=BC∧GNeighbVtxB=AC→GNeighbVtxC=AB
42 41 pm4.71d ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→GNeighbVtxA=BC∧GNeighbVtxB=AC↔GNeighbVtxA=BC∧GNeighbVtxB=AC∧GNeighbVtxC=AB
43 df-3an ⊢GNeighbVtxA=BC∧GNeighbVtxB=AC∧GNeighbVtxC=AB↔GNeighbVtxA=BC∧GNeighbVtxB=AC∧GNeighbVtxC=AB
44 42 43 bitr4di ⊢A∈X∧B∈Y∧C∈Z∧Vtx⁡G=ABC∧G∈USGraph→GNeighbVtxA=BC∧GNeighbVtxB=AC↔GNeighbVtxA=BC∧GNeighbVtxB=AC∧GNeighbVtxC=AB