# 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}=\mathrm{Vtx}\left({G}\right)$
nb3grpr.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
nb3grpr.g ${⊢}{\phi }\to {G}\in \mathrm{USGraph}$
nb3grpr.t ${⊢}{\phi }\to {V}=\left\{{A},{B},{C}\right\}$
nb3grpr.s ${⊢}{\phi }\to \left({A}\in {X}\wedge {B}\in {Y}\wedge {C}\in {Z}\right)$
nb3grpr.n ${⊢}{\phi }\to \left({A}\ne {B}\wedge {A}\ne {C}\wedge {B}\ne {C}\right)$
Assertion nb3grpr2 ${⊢}{\phi }\to \left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)↔\left({G}\mathrm{NeighbVtx}{A}=\left\{{B},{C}\right\}\wedge {G}\mathrm{NeighbVtx}{B}=\left\{{A},{C}\right\}\wedge {G}\mathrm{NeighbVtx}{C}=\left\{{A},{B}\right\}\right)\right)$

### Proof

Step Hyp Ref Expression
1 nb3grpr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 nb3grpr.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 nb3grpr.g ${⊢}{\phi }\to {G}\in \mathrm{USGraph}$
4 nb3grpr.t ${⊢}{\phi }\to {V}=\left\{{A},{B},{C}\right\}$
5 nb3grpr.s ${⊢}{\phi }\to \left({A}\in {X}\wedge {B}\in {Y}\wedge {C}\in {Z}\right)$
6 nb3grpr.n ${⊢}{\phi }\to \left({A}\ne {B}\wedge {A}\ne {C}\wedge {B}\ne {C}\right)$
7 3anan32 ${⊢}\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left\{{B},{C}\right\}\in {E}\right)$
8 7 a1i ${⊢}{\phi }\to \left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$
9 prcom ${⊢}\left\{{C},{A}\right\}=\left\{{A},{C}\right\}$
10 9 eleq1i ${⊢}\left\{{C},{A}\right\}\in {E}↔\left\{{A},{C}\right\}\in {E}$
11 10 biimpi ${⊢}\left\{{C},{A}\right\}\in {E}\to \left\{{A},{C}\right\}\in {E}$
12 11 pm4.71i ${⊢}\left\{{C},{A}\right\}\in {E}↔\left(\left\{{C},{A}\right\}\in {E}\wedge \left\{{A},{C}\right\}\in {E}\right)$
13 12 bianass ${⊢}\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left\{{A},{C}\right\}\in {E}\right)$
14 13 anbi1i ${⊢}\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left\{{B},{C}\right\}\in {E}\right)↔\left(\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left\{{A},{C}\right\}\in {E}\right)\wedge \left\{{B},{C}\right\}\in {E}\right)$
15 anass ${⊢}\left(\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left\{{A},{C}\right\}\in {E}\right)\wedge \left\{{B},{C}\right\}\in {E}\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$
16 14 15 bitri ${⊢}\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left\{{B},{C}\right\}\in {E}\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$
17 8 16 syl6bb ${⊢}{\phi }\to \left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)\right)$
18 prcom ${⊢}\left\{{A},{B}\right\}=\left\{{B},{A}\right\}$
19 18 eleq1i ${⊢}\left\{{A},{B}\right\}\in {E}↔\left\{{B},{A}\right\}\in {E}$
20 19 biimpi ${⊢}\left\{{A},{B}\right\}\in {E}\to \left\{{B},{A}\right\}\in {E}$
21 20 pm4.71i ${⊢}\left\{{A},{B}\right\}\in {E}↔\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{A}\right\}\in {E}\right)$
22 21 anbi1i ${⊢}\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{A}\right\}\in {E}\right)\wedge \left\{{C},{A}\right\}\in {E}\right)$
23 df-3an ${⊢}\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{A}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{A}\right\}\in {E}\right)\wedge \left\{{C},{A}\right\}\in {E}\right)$
24 22 23 bitr4i ${⊢}\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)↔\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{A}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)$
25 prcom ${⊢}\left\{{B},{C}\right\}=\left\{{C},{B}\right\}$
26 25 eleq1i ${⊢}\left\{{B},{C}\right\}\in {E}↔\left\{{C},{B}\right\}\in {E}$
27 26 biimpi ${⊢}\left\{{B},{C}\right\}\in {E}\to \left\{{C},{B}\right\}\in {E}$
28 27 pm4.71i ${⊢}\left\{{B},{C}\right\}\in {E}↔\left(\left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)$
29 28 anbi2i ${⊢}\left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)↔\left(\left\{{A},{C}\right\}\in {E}\wedge \left(\left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)\right)$
30 3anass ${⊢}\left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)↔\left(\left\{{A},{C}\right\}\in {E}\wedge \left(\left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)\right)$
31 29 30 bitr4i ${⊢}\left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)↔\left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)$
32 24 31 anbi12i ${⊢}\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{A}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)\right)$
33 an6 ${⊢}\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{A}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{A},{C}\right\}\in {E}\right)\wedge \left(\left\{{B},{A}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left(\left\{{C},{A}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)\right)$
34 32 33 bitri ${⊢}\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)\wedge \left(\left\{{A},{C}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{A},{C}\right\}\in {E}\right)\wedge \left(\left\{{B},{A}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left(\left\{{C},{A}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)\right)$
35 17 34 syl6bb ${⊢}{\phi }\to \left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{A},{C}\right\}\in {E}\right)\wedge \left(\left\{{B},{A}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left(\left\{{C},{A}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)\right)\right)$
36 1 2 3 4 5 nb3grprlem1 ${⊢}{\phi }\to \left({G}\mathrm{NeighbVtx}{A}=\left\{{B},{C}\right\}↔\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{A},{C}\right\}\in {E}\right)\right)$
37 tpcoma ${⊢}\left\{{A},{B},{C}\right\}=\left\{{B},{A},{C}\right\}$
38 4 37 syl6eq ${⊢}{\phi }\to {V}=\left\{{B},{A},{C}\right\}$
39 3ancoma ${⊢}\left({A}\in {X}\wedge {B}\in {Y}\wedge {C}\in {Z}\right)↔\left({B}\in {Y}\wedge {A}\in {X}\wedge {C}\in {Z}\right)$
40 5 39 sylib ${⊢}{\phi }\to \left({B}\in {Y}\wedge {A}\in {X}\wedge {C}\in {Z}\right)$
41 1 2 3 38 40 nb3grprlem1 ${⊢}{\phi }\to \left({G}\mathrm{NeighbVtx}{B}=\left\{{A},{C}\right\}↔\left(\left\{{B},{A}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\right)$
42 tprot ${⊢}\left\{{C},{A},{B}\right\}=\left\{{A},{B},{C}\right\}$
43 4 42 syl6eqr ${⊢}{\phi }\to {V}=\left\{{C},{A},{B}\right\}$
44 3anrot ${⊢}\left({C}\in {Z}\wedge {A}\in {X}\wedge {B}\in {Y}\right)↔\left({A}\in {X}\wedge {B}\in {Y}\wedge {C}\in {Z}\right)$
45 5 44 sylibr ${⊢}{\phi }\to \left({C}\in {Z}\wedge {A}\in {X}\wedge {B}\in {Y}\right)$
46 1 2 3 43 45 nb3grprlem1 ${⊢}{\phi }\to \left({G}\mathrm{NeighbVtx}{C}=\left\{{A},{B}\right\}↔\left(\left\{{C},{A}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)\right)$
47 36 41 46 3anbi123d ${⊢}{\phi }\to \left(\left({G}\mathrm{NeighbVtx}{A}=\left\{{B},{C}\right\}\wedge {G}\mathrm{NeighbVtx}{B}=\left\{{A},{C}\right\}\wedge {G}\mathrm{NeighbVtx}{C}=\left\{{A},{B}\right\}\right)↔\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{A},{C}\right\}\in {E}\right)\wedge \left(\left\{{B},{A}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left(\left\{{C},{A}\right\}\in {E}\wedge \left\{{C},{B}\right\}\in {E}\right)\right)\right)$
48 35 47 bitr4d ${⊢}{\phi }\to \left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\wedge \left\{{C},{A}\right\}\in {E}\right)↔\left({G}\mathrm{NeighbVtx}{A}=\left\{{B},{C}\right\}\wedge {G}\mathrm{NeighbVtx}{B}=\left\{{A},{C}\right\}\wedge {G}\mathrm{NeighbVtx}{C}=\left\{{A},{B}\right\}\right)\right)$