Metamath Proof Explorer

Theorem nb3grpr

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 nb3grpr ⊢ φ → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ ∀ x ∈ V ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z

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 id ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E
8 prcom ⊢ A B = B A
9 8 eleq1i ⊢ A B ∈ E ↔ B A ∈ E
10 prcom ⊢ B C = C B
11 10 eleq1i ⊢ B C ∈ E ↔ C B ∈ E
12 prcom ⊢ C A = A C
13 12 eleq1i ⊢ C A ∈ E ↔ A C ∈ E
14 9 11 13 3anbi123i ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ B A ∈ E ∧ C B ∈ E ∧ A C ∈ E
15 3anrot ⊢ A C ∈ E ∧ B A ∈ E ∧ C B ∈ E ↔ B A ∈ E ∧ C B ∈ E ∧ A C ∈ E
16 14 15 bitr4i ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ A C ∈ E ∧ B A ∈ E ∧ C B ∈ E
17 16 a1i ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ A C ∈ E ∧ B A ∈ E ∧ C B ∈ E
18 7 17 biadanii ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A C ∈ E ∧ B A ∈ E ∧ C B ∈ E
19 an6 ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ∧ A C ∈ E ∧ B A ∈ E ∧ C B ∈ E ↔ A B ∈ E ∧ A C ∈ E ∧ B C ∈ E ∧ B A ∈ E ∧ C A ∈ E ∧ C B ∈ E
20 18 19 bitri ⊢ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ A B ∈ E ∧ A C ∈ E ∧ B C ∈ E ∧ B A ∈ E ∧ C A ∈ E ∧ C B ∈ E
21 20 a1i ⊢ φ → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ A B ∈ E ∧ A C ∈ E ∧ B C ∈ E ∧ B A ∈ E ∧ C A ∈ E ∧ C B ∈ E
22 1 2 3 4 5 nb3grprlem1 ⊢ φ → G NeighbVtx A = B C ↔ A B ∈ E ∧ A C ∈ E
23 tprot ⊢ A B C = B C A
24 4 23 eqtrdi ⊢ φ → V = B C A
25 3anrot ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ↔ B ∈ Y ∧ C ∈ Z ∧ A ∈ X
26 5 25 sylib ⊢ φ → B ∈ Y ∧ C ∈ Z ∧ A ∈ X
27 1 2 3 24 26 nb3grprlem1 ⊢ φ → G NeighbVtx B = C A ↔ B C ∈ E ∧ B A ∈ E
28 tprot ⊢ C A B = A B C
29 4 28 eqtr4di ⊢ φ → V = C A B
30 3anrot ⊢ C ∈ Z ∧ A ∈ X ∧ B ∈ Y ↔ A ∈ X ∧ B ∈ Y ∧ C ∈ Z
31 5 30 sylibr ⊢ φ → C ∈ Z ∧ A ∈ X ∧ B ∈ Y
32 1 2 3 29 31 nb3grprlem1 ⊢ φ → G NeighbVtx C = A B ↔ C A ∈ E ∧ C B ∈ E
33 22 27 32 3anbi123d ⊢ φ → G NeighbVtx A = B C ∧ G NeighbVtx B = C A ∧ G NeighbVtx C = A B ↔ A B ∈ E ∧ A C ∈ E ∧ B C ∈ E ∧ B A ∈ E ∧ C A ∈ E ∧ C B ∈ E
34 1 2 3 4 5 6 nb3grprlem2 ⊢ φ → G NeighbVtx A = B C ↔ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx A = y z
35 necom ⊢ A ≠ B ↔ B ≠ A
36 necom ⊢ A ≠ C ↔ C ≠ A
37 biid ⊢ B ≠ C ↔ B ≠ C
38 35 36 37 3anbi123i ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C ↔ B ≠ A ∧ C ≠ A ∧ B ≠ C
39 3anrot ⊢ B ≠ C ∧ B ≠ A ∧ C ≠ A ↔ B ≠ A ∧ C ≠ A ∧ B ≠ C
40 38 39 bitr4i ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C ↔ B ≠ C ∧ B ≠ A ∧ C ≠ A
41 6 40 sylib ⊢ φ → B ≠ C ∧ B ≠ A ∧ C ≠ A
42 1 2 3 24 26 41 nb3grprlem2 ⊢ φ → G NeighbVtx B = C A ↔ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx B = y z
43 3anrot ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C ↔ A ≠ C ∧ B ≠ C ∧ A ≠ B
44 necom ⊢ B ≠ C ↔ C ≠ B
45 biid ⊢ A ≠ B ↔ A ≠ B
46 36 44 45 3anbi123i ⊢ A ≠ C ∧ B ≠ C ∧ A ≠ B ↔ C ≠ A ∧ C ≠ B ∧ A ≠ B
47 43 46 bitri ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C ↔ C ≠ A ∧ C ≠ B ∧ A ≠ B
48 6 47 sylib ⊢ φ → C ≠ A ∧ C ≠ B ∧ A ≠ B
49 1 2 3 29 31 48 nb3grprlem2 ⊢ φ → G NeighbVtx C = A B ↔ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx C = y z
50 34 42 49 3anbi123d ⊢ φ → G NeighbVtx A = B C ∧ G NeighbVtx B = C A ∧ G NeighbVtx C = A B ↔ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx A = y z ∧ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx B = y z ∧ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx C = y z
51 21 33 50 3bitr2d ⊢ φ → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx A = y z ∧ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx B = y z ∧ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx C = y z
52 oveq2 ⊢ x = A → G NeighbVtx x = G NeighbVtx A
53 52 eqeq1d ⊢ x = A → G NeighbVtx x = y z ↔ G NeighbVtx A = y z
54 53 2rexbidv ⊢ x = A → ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z ↔ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx A = y z
55 oveq2 ⊢ x = B → G NeighbVtx x = G NeighbVtx B
56 55 eqeq1d ⊢ x = B → G NeighbVtx x = y z ↔ G NeighbVtx B = y z
57 56 2rexbidv ⊢ x = B → ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z ↔ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx B = y z
58 oveq2 ⊢ x = C → G NeighbVtx x = G NeighbVtx C
59 58 eqeq1d ⊢ x = C → G NeighbVtx x = y z ↔ G NeighbVtx C = y z
60 59 2rexbidv ⊢ x = C → ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z ↔ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx C = y z
61 54 57 60 raltpg ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∀ x ∈ A B C ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z ↔ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx A = y z ∧ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx B = y z ∧ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx C = y z
62 5 61 syl ⊢ φ → ∀ x ∈ A B C ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z ↔ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx A = y z ∧ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx B = y z ∧ ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx C = y z
63 raleq ⊢ V = A B C → ∀ x ∈ V ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z ↔ ∀ x ∈ A B C ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z
64 63 bicomd ⊢ V = A B C → ∀ x ∈ A B C ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z ↔ ∀ x ∈ V ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z
65 4 64 syl ⊢ φ → ∀ x ∈ A B C ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z ↔ ∀ x ∈ V ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z
66 51 62 65 3bitr2d ⊢ φ → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ ∀ x ∈ V ∃ y ∈ V ∃ z ∈ V ∖ y G NeighbVtx x = y z