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 = A B C
nb3grpr.s φ A X B Y C Z
nb3grpr.n φ A B A C B C
Assertion nb3grpr2 φ A B E B C E C A E G NeighbVtx A = B C G NeighbVtx B = A C G NeighbVtx C = A B

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 = A B C
5 nb3grpr.s φ A X B Y C Z
6 nb3grpr.n φ A B A C B C
7 3anan32 A B E B C E C A E A B E C A E B C E
8 7 a1i φ A B E B C E C A E A B E C A E B C E
9 prcom C A = A C
10 9 eleq1i C A E A C E
11 10 biimpi C A E A C E
12 11 pm4.71i C A E C A E A C E
13 12 bianass A B E C A E A B E C A E A C E
14 13 anbi1i A B E C A E B C E A B E C A E A C E B C E
15 anass A B E C A E A C E B C E A B E C A E A C E B C E
16 14 15 bitri A B E C A E B C E A B E C A E A C E B C E
17 8 16 syl6bb φ A B E B C E C A E A B E C A E A C E B C E
18 prcom A B = B A
19 18 eleq1i A B E B A E
20 19 biimpi A B E B A E
21 20 pm4.71i A B E A B E B A E
22 21 anbi1i A B E C A E A B E B A E C A E
23 df-3an A B E B A E C A E A B E B A E C A E
24 22 23 bitr4i A B E C A E A B E B A E C A E
25 prcom B C = C B
26 25 eleq1i B C E C B E
27 26 biimpi B C E C B E
28 27 pm4.71i B C E B C E C B E
29 28 anbi2i A C E B C E A C E B C E C B E
30 3anass A C E B C E C B E A C E B C E C B E
31 29 30 bitr4i A C E B C E A C E B C E C B E
32 24 31 anbi12i A B E C A E A C E B C E A B E B A E C A E A C E B C E C B E
33 an6 A B E B A E C A E A C E B C E C B E A B E A C E B A E B C E C A E C B E
34 32 33 bitri A B E C A E A C E B C E A B E A C E B A E B C E C A E C B E
35 17 34 syl6bb φ A B E B C E C A E A B E A C E B A E B C E C A E C B E
36 1 2 3 4 5 nb3grprlem1 φ G NeighbVtx A = B C A B E A C E
37 tpcoma A B C = B A C
38 4 37 syl6eq φ V = B A C
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 φ G NeighbVtx B = A C B A E B C E
42 tprot C A B = A B C
43 4 42 syl6eqr φ V = C A B
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 φ G NeighbVtx C = A B C A E C B E
47 36 41 46 3anbi123d φ G NeighbVtx A = B C G NeighbVtx B = A C G NeighbVtx C = A B A B E A C E B A E B C E C A E C B E
48 35 47 bitr4d φ A B E B C E C A E G NeighbVtx A = B C G NeighbVtx B = A C G NeighbVtx C = A B