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 bitrdi ⊢ φ → 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 bitrdi ⊢ φ → 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 eqtrdi ⊢ φ → 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 eqtr4di ⊢ φ → 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