Metamath Proof Explorer


Theorem nb3grprlem2

Description: Lemma 2 for nb3grpr . (Contributed by Alexander van der Vekens, 17-Oct-2017) (Revised by AV, 28-Oct-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nb3grpr.v V=VtxG
nb3grpr.e E=EdgG
nb3grpr.g φGUSGraph
nb3grpr.t φV=ABC
nb3grpr.s φAXBYCZ
nb3grpr.n φABACBC
Assertion nb3grprlem2 φGNeighbVtxA=BCvVwVvGNeighbVtxA=vw

Proof

Step Hyp Ref Expression
1 nb3grpr.v V=VtxG
2 nb3grpr.e E=EdgG
3 nb3grpr.g φGUSGraph
4 nb3grpr.t φV=ABC
5 nb3grpr.s φAXBYCZ
6 nb3grpr.n φABACBC
7 sneq v=Av=A
8 7 difeq2d v=AABCv=ABCA
9 preq1 v=Avw=Aw
10 9 eqeq2d v=AGNeighbVtxA=vwGNeighbVtxA=Aw
11 8 10 rexeqbidv v=AwABCvGNeighbVtxA=vwwABCAGNeighbVtxA=Aw
12 sneq v=Bv=B
13 12 difeq2d v=BABCv=ABCB
14 preq1 v=Bvw=Bw
15 14 eqeq2d v=BGNeighbVtxA=vwGNeighbVtxA=Bw
16 13 15 rexeqbidv v=BwABCvGNeighbVtxA=vwwABCBGNeighbVtxA=Bw
17 sneq v=Cv=C
18 17 difeq2d v=CABCv=ABCC
19 preq1 v=Cvw=Cw
20 19 eqeq2d v=CGNeighbVtxA=vwGNeighbVtxA=Cw
21 18 20 rexeqbidv v=CwABCvGNeighbVtxA=vwwABCCGNeighbVtxA=Cw
22 11 16 21 rextpg AXBYCZvABCwABCvGNeighbVtxA=vwwABCAGNeighbVtxA=AwwABCBGNeighbVtxA=BwwABCCGNeighbVtxA=Cw
23 5 22 syl φvABCwABCvGNeighbVtxA=vwwABCAGNeighbVtxA=AwwABCBGNeighbVtxA=BwwABCCGNeighbVtxA=Cw
24 4 3 jca φV=ABCGUSGraph
25 simpl V=ABCGUSGraphV=ABC
26 difeq1 V=ABCVv=ABCv
27 26 adantr V=ABCGUSGraphVv=ABCv
28 27 rexeqdv V=ABCGUSGraphwVvGNeighbVtxA=vwwABCvGNeighbVtxA=vw
29 25 28 rexeqbidv V=ABCGUSGraphvVwVvGNeighbVtxA=vwvABCwABCvGNeighbVtxA=vw
30 24 29 syl φvVwVvGNeighbVtxA=vwvABCwABCvGNeighbVtxA=vw
31 preq2 w=BAw=AB
32 31 eqeq2d w=BGNeighbVtxA=AwGNeighbVtxA=AB
33 preq2 w=CAw=AC
34 33 eqeq2d w=CGNeighbVtxA=AwGNeighbVtxA=AC
35 32 34 rexprg BYCZwBCGNeighbVtxA=AwGNeighbVtxA=ABGNeighbVtxA=AC
36 35 3adant1 AXBYCZwBCGNeighbVtxA=AwGNeighbVtxA=ABGNeighbVtxA=AC
37 preq2 w=CBw=BC
38 37 eqeq2d w=CGNeighbVtxA=BwGNeighbVtxA=BC
39 preq2 w=ABw=BA
40 39 eqeq2d w=AGNeighbVtxA=BwGNeighbVtxA=BA
41 38 40 rexprg CZAXwCAGNeighbVtxA=BwGNeighbVtxA=BCGNeighbVtxA=BA
42 41 ancoms AXCZwCAGNeighbVtxA=BwGNeighbVtxA=BCGNeighbVtxA=BA
43 42 3adant2 AXBYCZwCAGNeighbVtxA=BwGNeighbVtxA=BCGNeighbVtxA=BA
44 preq2 w=ACw=CA
45 44 eqeq2d w=AGNeighbVtxA=CwGNeighbVtxA=CA
46 preq2 w=BCw=CB
47 46 eqeq2d w=BGNeighbVtxA=CwGNeighbVtxA=CB
48 45 47 rexprg AXBYwABGNeighbVtxA=CwGNeighbVtxA=CAGNeighbVtxA=CB
49 48 3adant3 AXBYCZwABGNeighbVtxA=CwGNeighbVtxA=CAGNeighbVtxA=CB
50 36 43 49 3orbi123d AXBYCZwBCGNeighbVtxA=AwwCAGNeighbVtxA=BwwABGNeighbVtxA=CwGNeighbVtxA=ABGNeighbVtxA=ACGNeighbVtxA=BCGNeighbVtxA=BAGNeighbVtxA=CAGNeighbVtxA=CB
51 5 50 syl φwBCGNeighbVtxA=AwwCAGNeighbVtxA=BwwABGNeighbVtxA=CwGNeighbVtxA=ABGNeighbVtxA=ACGNeighbVtxA=BCGNeighbVtxA=BAGNeighbVtxA=CAGNeighbVtxA=CB
52 tprot ABC=BCA
53 52 a1i ABACBCABC=BCA
54 53 difeq1d ABACBCABCA=BCAA
55 necom ABBA
56 necom ACCA
57 diftpsn3 BACABCAA=BC
58 55 56 57 syl2anb ABACBCAA=BC
59 58 3adant3 ABACBCBCAA=BC
60 54 59 eqtrd ABACBCABCA=BC
61 60 rexeqdv ABACBCwABCAGNeighbVtxA=AwwBCGNeighbVtxA=Aw
62 tprot CAB=ABC
63 62 eqcomi ABC=CAB
64 63 a1i ABACBCABC=CAB
65 64 difeq1d ABACBCABCB=CABB
66 necom BCCB
67 66 anbi1i BCABCBAB
68 67 biimpi BCABCBAB
69 68 ancoms ABBCCBAB
70 diftpsn3 CBABCABB=CA
71 69 70 syl ABBCCABB=CA
72 71 3adant2 ABACBCCABB=CA
73 65 72 eqtrd ABACBCABCB=CA
74 73 rexeqdv ABACBCwABCBGNeighbVtxA=BwwCAGNeighbVtxA=Bw
75 diftpsn3 ACBCABCC=AB
76 75 3adant1 ABACBCABCC=AB
77 76 rexeqdv ABACBCwABCCGNeighbVtxA=CwwABGNeighbVtxA=Cw
78 61 74 77 3orbi123d ABACBCwABCAGNeighbVtxA=AwwABCBGNeighbVtxA=BwwABCCGNeighbVtxA=CwwBCGNeighbVtxA=AwwCAGNeighbVtxA=BwwABGNeighbVtxA=Cw
79 6 78 syl φwABCAGNeighbVtxA=AwwABCBGNeighbVtxA=BwwABCCGNeighbVtxA=CwwBCGNeighbVtxA=AwwCAGNeighbVtxA=BwwABGNeighbVtxA=Cw
80 prcom CB=BC
81 80 eqeq2i GNeighbVtxA=CBGNeighbVtxA=BC
82 81 orbi2i GNeighbVtxA=BCGNeighbVtxA=CBGNeighbVtxA=BCGNeighbVtxA=BC
83 oridm GNeighbVtxA=BCGNeighbVtxA=BCGNeighbVtxA=BC
84 82 83 bitr2i GNeighbVtxA=BCGNeighbVtxA=BCGNeighbVtxA=CB
85 84 a1i φGNeighbVtxA=BCGNeighbVtxA=BCGNeighbVtxA=CB
86 nbgrnself2 AGNeighbVtxA
87 df-nel AGNeighbVtxA¬AGNeighbVtxA
88 prid2g AXABA
89 88 3ad2ant1 AXBYCZABA
90 eleq2 GNeighbVtxA=BAAGNeighbVtxAABA
91 89 90 syl5ibrcom AXBYCZGNeighbVtxA=BAAGNeighbVtxA
92 91 con3rr3 ¬AGNeighbVtxAAXBYCZ¬GNeighbVtxA=BA
93 87 92 sylbi AGNeighbVtxAAXBYCZ¬GNeighbVtxA=BA
94 86 5 93 mpsyl φ¬GNeighbVtxA=BA
95 biorf ¬GNeighbVtxA=BAGNeighbVtxA=BCGNeighbVtxA=BAGNeighbVtxA=BC
96 orcom GNeighbVtxA=BAGNeighbVtxA=BCGNeighbVtxA=BCGNeighbVtxA=BA
97 95 96 bitrdi ¬GNeighbVtxA=BAGNeighbVtxA=BCGNeighbVtxA=BCGNeighbVtxA=BA
98 94 97 syl φGNeighbVtxA=BCGNeighbVtxA=BCGNeighbVtxA=BA
99 prid2g AXACA
100 99 3ad2ant1 AXBYCZACA
101 eleq2 GNeighbVtxA=CAAGNeighbVtxAACA
102 100 101 syl5ibrcom AXBYCZGNeighbVtxA=CAAGNeighbVtxA
103 102 con3rr3 ¬AGNeighbVtxAAXBYCZ¬GNeighbVtxA=CA
104 87 103 sylbi AGNeighbVtxAAXBYCZ¬GNeighbVtxA=CA
105 86 5 104 mpsyl φ¬GNeighbVtxA=CA
106 biorf ¬GNeighbVtxA=CAGNeighbVtxA=CBGNeighbVtxA=CAGNeighbVtxA=CB
107 105 106 syl φGNeighbVtxA=CBGNeighbVtxA=CAGNeighbVtxA=CB
108 98 107 orbi12d φGNeighbVtxA=BCGNeighbVtxA=CBGNeighbVtxA=BCGNeighbVtxA=BAGNeighbVtxA=CAGNeighbVtxA=CB
109 prid1g AXAAB
110 109 3ad2ant1 AXBYCZAAB
111 eleq2 GNeighbVtxA=ABAGNeighbVtxAAAB
112 110 111 syl5ibrcom AXBYCZGNeighbVtxA=ABAGNeighbVtxA
113 112 con3dimp AXBYCZ¬AGNeighbVtxA¬GNeighbVtxA=AB
114 prid1g AXAAC
115 114 3ad2ant1 AXBYCZAAC
116 eleq2 GNeighbVtxA=ACAGNeighbVtxAAAC
117 115 116 syl5ibrcom AXBYCZGNeighbVtxA=ACAGNeighbVtxA
118 117 con3dimp AXBYCZ¬AGNeighbVtxA¬GNeighbVtxA=AC
119 113 118 jca AXBYCZ¬AGNeighbVtxA¬GNeighbVtxA=AB¬GNeighbVtxA=AC
120 119 expcom ¬AGNeighbVtxAAXBYCZ¬GNeighbVtxA=AB¬GNeighbVtxA=AC
121 87 120 sylbi AGNeighbVtxAAXBYCZ¬GNeighbVtxA=AB¬GNeighbVtxA=AC
122 86 5 121 mpsyl φ¬GNeighbVtxA=AB¬GNeighbVtxA=AC
123 ioran ¬GNeighbVtxA=ABGNeighbVtxA=AC¬GNeighbVtxA=AB¬GNeighbVtxA=AC
124 122 123 sylibr φ¬GNeighbVtxA=ABGNeighbVtxA=AC
125 124 3bior1fd φGNeighbVtxA=BCGNeighbVtxA=BAGNeighbVtxA=CAGNeighbVtxA=CBGNeighbVtxA=ABGNeighbVtxA=ACGNeighbVtxA=BCGNeighbVtxA=BAGNeighbVtxA=CAGNeighbVtxA=CB
126 85 108 125 3bitrd φGNeighbVtxA=BCGNeighbVtxA=ABGNeighbVtxA=ACGNeighbVtxA=BCGNeighbVtxA=BAGNeighbVtxA=CAGNeighbVtxA=CB
127 51 79 126 3bitr4rd φGNeighbVtxA=BCwABCAGNeighbVtxA=AwwABCBGNeighbVtxA=BwwABCCGNeighbVtxA=Cw
128 23 30 127 3bitr4rd φGNeighbVtxA=BCvVwVvGNeighbVtxA=vw