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=ABC
nb3grpr.s ⊢φ→A∈X∧B∈Y∧C∈Z
nb3grpr.n ⊢φ→A≠B∧A≠C∧B≠C
Assertion nb3grpr ⊢φ→AB∈E∧BC∈E∧CA∈E↔∀x∈V∃y∈V∃z∈V∖yGNeighbVtxx=yz

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 id ⊢AB∈E∧BC∈E∧CA∈E→AB∈E∧BC∈E∧CA∈E
8 prcom ⊢AB=BA
9 8 eleq1i ⊢AB∈E↔BA∈E
10 prcom ⊢BC=CB
11 10 eleq1i ⊢BC∈E↔CB∈E
12 prcom ⊢CA=AC
13 12 eleq1i ⊢CA∈E↔AC∈E
14 9 11 13 3anbi123i ⊢AB∈E∧BC∈E∧CA∈E↔BA∈E∧CB∈E∧AC∈E
15 3anrot ⊢AC∈E∧BA∈E∧CB∈E↔BA∈E∧CB∈E∧AC∈E
16 14 15 bitr4i ⊢AB∈E∧BC∈E∧CA∈E↔AC∈E∧BA∈E∧CB∈E
17 16 a1i ⊢AB∈E∧BC∈E∧CA∈E→AB∈E∧BC∈E∧CA∈E↔AC∈E∧BA∈E∧CB∈E
18 7 17 biadanii ⊢AB∈E∧BC∈E∧CA∈E↔AB∈E∧BC∈E∧CA∈E∧AC∈E∧BA∈E∧CB∈E
19 an6 ⊢AB∈E∧BC∈E∧CA∈E∧AC∈E∧BA∈E∧CB∈E↔AB∈E∧AC∈E∧BC∈E∧BA∈E∧CA∈E∧CB∈E
20 18 19 bitri ⊢AB∈E∧BC∈E∧CA∈E↔AB∈E∧AC∈E∧BC∈E∧BA∈E∧CA∈E∧CB∈E
21 20 a1i ⊢φ→AB∈E∧BC∈E∧CA∈E↔AB∈E∧AC∈E∧BC∈E∧BA∈E∧CA∈E∧CB∈E
22 1 2 3 4 5 nb3grprlem1 ⊢φ→GNeighbVtxA=BC↔AB∈E∧AC∈E
23 tprot ⊢ABC=BCA
24 4 23 eqtrdi ⊢φ→V=BCA
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 ⊢φ→GNeighbVtxB=CA↔BC∈E∧BA∈E
28 tprot ⊢CAB=ABC
29 4 28 eqtr4di ⊢φ→V=CAB
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 ⊢φ→GNeighbVtxC=AB↔CA∈E∧CB∈E
33 22 27 32 3anbi123d ⊢φ→GNeighbVtxA=BC∧GNeighbVtxB=CA∧GNeighbVtxC=AB↔AB∈E∧AC∈E∧BC∈E∧BA∈E∧CA∈E∧CB∈E
34 1 2 3 4 5 6 nb3grprlem2 ⊢φ→GNeighbVtxA=BC↔∃y∈V∃z∈V∖yGNeighbVtxA=yz
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 ⊢φ→GNeighbVtxB=CA↔∃y∈V∃z∈V∖yGNeighbVtxB=yz
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 ⊢φ→GNeighbVtxC=AB↔∃y∈V∃z∈V∖yGNeighbVtxC=yz
50 34 42 49 3anbi123d ⊢φ→GNeighbVtxA=BC∧GNeighbVtxB=CA∧GNeighbVtxC=AB↔∃y∈V∃z∈V∖yGNeighbVtxA=yz∧∃y∈V∃z∈V∖yGNeighbVtxB=yz∧∃y∈V∃z∈V∖yGNeighbVtxC=yz
51 21 33 50 3bitr2d ⊢φ→AB∈E∧BC∈E∧CA∈E↔∃y∈V∃z∈V∖yGNeighbVtxA=yz∧∃y∈V∃z∈V∖yGNeighbVtxB=yz∧∃y∈V∃z∈V∖yGNeighbVtxC=yz
52 oveq2 ⊢x=A→GNeighbVtxx=GNeighbVtxA
53 52 eqeq1d ⊢x=A→GNeighbVtxx=yz↔GNeighbVtxA=yz
54 53 2rexbidv ⊢x=A→∃y∈V∃z∈V∖yGNeighbVtxx=yz↔∃y∈V∃z∈V∖yGNeighbVtxA=yz
55 oveq2 ⊢x=B→GNeighbVtxx=GNeighbVtxB
56 55 eqeq1d ⊢x=B→GNeighbVtxx=yz↔GNeighbVtxB=yz
57 56 2rexbidv ⊢x=B→∃y∈V∃z∈V∖yGNeighbVtxx=yz↔∃y∈V∃z∈V∖yGNeighbVtxB=yz
58 oveq2 ⊢x=C→GNeighbVtxx=GNeighbVtxC
59 58 eqeq1d ⊢x=C→GNeighbVtxx=yz↔GNeighbVtxC=yz
60 59 2rexbidv ⊢x=C→∃y∈V∃z∈V∖yGNeighbVtxx=yz↔∃y∈V∃z∈V∖yGNeighbVtxC=yz
61 54 57 60 raltpg ⊢A∈X∧B∈Y∧C∈Z→∀x∈ABC∃y∈V∃z∈V∖yGNeighbVtxx=yz↔∃y∈V∃z∈V∖yGNeighbVtxA=yz∧∃y∈V∃z∈V∖yGNeighbVtxB=yz∧∃y∈V∃z∈V∖yGNeighbVtxC=yz
62 5 61 syl ⊢φ→∀x∈ABC∃y∈V∃z∈V∖yGNeighbVtxx=yz↔∃y∈V∃z∈V∖yGNeighbVtxA=yz∧∃y∈V∃z∈V∖yGNeighbVtxB=yz∧∃y∈V∃z∈V∖yGNeighbVtxC=yz
63 raleq ⊢V=ABC→∀x∈V∃y∈V∃z∈V∖yGNeighbVtxx=yz↔∀x∈ABC∃y∈V∃z∈V∖yGNeighbVtxx=yz
64 63 bicomd ⊢V=ABC→∀x∈ABC∃y∈V∃z∈V∖yGNeighbVtxx=yz↔∀x∈V∃y∈V∃z∈V∖yGNeighbVtxx=yz
65 4 64 syl ⊢φ→∀x∈ABC∃y∈V∃z∈V∖yGNeighbVtxx=yz↔∀x∈V∃y∈V∃z∈V∖yGNeighbVtxx=yz
66 51 62 65 3bitr2d ⊢φ→AB∈E∧BC∈E∧CA∈E↔∀x∈V∃y∈V∃z∈V∖yGNeighbVtxx=yz