Metamath Proof Explorer

Theorem nb3grpr2

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

Ref Expression
Hypotheses nb3grpr.v ⊢V=Vtx⁡G
nb3grpr.e ⊢E=Edg⁡G
nb3grpr.g ⊢φ→G∈USGraph
nb3grpr.t ⊢φ→V=ABC
nb3grpr.s ⊢φ→A∈X∧B∈Y∧C∈Z
nb3grpr.n ⊢φ→A≠B∧A≠C∧B≠C
Assertion nb3grpr2 ⊢φ→AB∈E∧BC∈E∧CA∈E↔GNeighbVtxA=BC∧GNeighbVtxB=AC∧GNeighbVtxC=AB

Proof

Step Hyp Ref Expression
1 nb3grpr.v ⊢V=Vtx⁡G
2 nb3grpr.e ⊢E=Edg⁡G
3 nb3grpr.g ⊢φ→G∈USGraph
4 nb3grpr.t ⊢φ→V=ABC
5 nb3grpr.s ⊢φ→A∈X∧B∈Y∧C∈Z
6 nb3grpr.n ⊢φ→A≠B∧A≠C∧B≠C
7 3anan32 ⊢AB∈E∧BC∈E∧CA∈E↔AB∈E∧CA∈E∧BC∈E
8 7 a1i ⊢φ→AB∈E∧BC∈E∧CA∈E↔AB∈E∧CA∈E∧BC∈E
9 prcom ⊢CA=AC
10 9 eleq1i ⊢CA∈E↔AC∈E
11 10 biimpi ⊢CA∈E→AC∈E
12 11 pm4.71i ⊢CA∈E↔CA∈E∧AC∈E
13 12 bianass ⊢AB∈E∧CA∈E↔AB∈E∧CA∈E∧AC∈E
14 13 anbi1i ⊢AB∈E∧CA∈E∧BC∈E↔AB∈E∧CA∈E∧AC∈E∧BC∈E
15 anass ⊢AB∈E∧CA∈E∧AC∈E∧BC∈E↔AB∈E∧CA∈E∧AC∈E∧BC∈E
16 14 15 bitri ⊢AB∈E∧CA∈E∧BC∈E↔AB∈E∧CA∈E∧AC∈E∧BC∈E
17 8 16 bitrdi ⊢φ→AB∈E∧BC∈E∧CA∈E↔AB∈E∧CA∈E∧AC∈E∧BC∈E
18 prcom ⊢AB=BA
19 18 eleq1i ⊢AB∈E↔BA∈E
20 19 biimpi ⊢AB∈E→BA∈E
21 20 pm4.71i ⊢AB∈E↔AB∈E∧BA∈E
22 21 anbi1i ⊢AB∈E∧CA∈E↔AB∈E∧BA∈E∧CA∈E
23 df-3an ⊢AB∈E∧BA∈E∧CA∈E↔AB∈E∧BA∈E∧CA∈E
24 22 23 bitr4i ⊢AB∈E∧CA∈E↔AB∈E∧BA∈E∧CA∈E
25 prcom ⊢BC=CB
26 25 eleq1i ⊢BC∈E↔CB∈E
27 26 biimpi ⊢BC∈E→CB∈E
28 27 pm4.71i ⊢BC∈E↔BC∈E∧CB∈E
29 28 anbi2i ⊢AC∈E∧BC∈E↔AC∈E∧BC∈E∧CB∈E
30 3anass ⊢AC∈E∧BC∈E∧CB∈E↔AC∈E∧BC∈E∧CB∈E
31 29 30 bitr4i ⊢AC∈E∧BC∈E↔AC∈E∧BC∈E∧CB∈E
32 24 31 anbi12i ⊢AB∈E∧CA∈E∧AC∈E∧BC∈E↔AB∈E∧BA∈E∧CA∈E∧AC∈E∧BC∈E∧CB∈E
33 an6 ⊢AB∈E∧BA∈E∧CA∈E∧AC∈E∧BC∈E∧CB∈E↔AB∈E∧AC∈E∧BA∈E∧BC∈E∧CA∈E∧CB∈E
34 32 33 bitri ⊢AB∈E∧CA∈E∧AC∈E∧BC∈E↔AB∈E∧AC∈E∧BA∈E∧BC∈E∧CA∈E∧CB∈E
35 17 34 bitrdi ⊢φ→AB∈E∧BC∈E∧CA∈E↔AB∈E∧AC∈E∧BA∈E∧BC∈E∧CA∈E∧CB∈E
36 1 2 3 4 5 nb3grprlem1 ⊢φ→GNeighbVtxA=BC↔AB∈E∧AC∈E
37 tpcoma ⊢ABC=BAC
38 4 37 eqtrdi ⊢φ→V=BAC
39 3ancoma ⊢A∈X∧B∈Y∧C∈Z↔B∈Y∧A∈X∧C∈Z
40 5 39 sylib ⊢φ→B∈Y∧A∈X∧C∈Z
41 1 2 3 38 40 nb3grprlem1 ⊢φ→GNeighbVtxB=AC↔BA∈E∧BC∈E
42 tprot ⊢CAB=ABC
43 4 42 eqtr4di ⊢φ→V=CAB
44 3anrot ⊢C∈Z∧A∈X∧B∈Y↔A∈X∧B∈Y∧C∈Z
45 5 44 sylibr ⊢φ→C∈Z∧A∈X∧B∈Y
46 1 2 3 43 45 nb3grprlem1 ⊢φ→GNeighbVtxC=AB↔CA∈E∧CB∈E
47 36 41 46 3anbi123d ⊢φ→GNeighbVtxA=BC∧GNeighbVtxB=AC∧GNeighbVtxC=AB↔AB∈E∧AC∈E∧BA∈E∧BC∈E∧CA∈E∧CB∈E
48 35 47 bitr4d ⊢φ→AB∈E∧BC∈E∧CA∈E↔GNeighbVtxA=BC∧GNeighbVtxB=AC∧GNeighbVtxC=AB