Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  usg2spot2nb Structured version   Unicode version

Theorem usg2spot2nb 28454
 Description: The set of paths of length 2 with a given vertex in the middle for a finite graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018.)
Hypothesis
Ref Expression
usgreghash2spot.m 2SPathOnOt
Assertion
Ref Expression
usg2spot2nb USGrph Neighbors Neighbors
Distinct variable groups:   ,,,   ,,,,   ,,,,   ,
Allowed substitution hints:   (,,,)

Proof of Theorem usg2spot2nb
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 959 . . . . 5 USGrph
2 3xpexg 28054 . . . . . . 7
3 rabexg 4353 . . . . . . 7 2SPathOnOt
42, 3syl 16 . . . . . 6 2SPathOnOt
543ad2ant2 979 . . . . 5 USGrph 2SPathOnOt
6 eqeq2 2445 . . . . . . . . 9
76anbi2d 685 . . . . . . . 8 2SPathOnOt 2SPathOnOt
87rabbidv 2948 . . . . . . 7 2SPathOnOt 2SPathOnOt
9 usgreghash2spot.m . . . . . . 7 2SPathOnOt
108, 9fvmptg 5804 . . . . . 6 2SPathOnOt 2SPathOnOt
1110eleq2d 2503 . . . . 5 2SPathOnOt 2SPathOnOt
121, 5, 11syl2anc 643 . . . 4 USGrph 2SPathOnOt
13 eleq1 2496 . . . . . . . 8 2SPathOnOt 2SPathOnOt
14 fveq2 5728 . . . . . . . . . 10
1514fveq2d 5732 . . . . . . . . 9
1615eqeq1d 2444 . . . . . . . 8
1713, 16anbi12d 692 . . . . . . 7 2SPathOnOt 2SPathOnOt
1817elrab 3092 . . . . . 6 2SPathOnOt 2SPathOnOt
1918a1i 11 . . . . 5 USGrph 2SPathOnOt 2SPathOnOt
20 usgrav 21371 . . . . . . . . . 10 USGrph
21 el2spthsoton 28346 . . . . . . . . . 10 2SPathOnOt 2SPathOnOt
2220, 21syl 16 . . . . . . . . 9 USGrph 2SPathOnOt 2SPathOnOt
23223ad2ant1 978 . . . . . . . 8 USGrph 2SPathOnOt 2SPathOnOt
24 usg2spthonot1 28357 . . . . . . . . . 10 USGrph 2SPathOnOt
25243ad2antl1 1119 . . . . . . . . 9 USGrph 2SPathOnOt
26252rexbidva 2746 . . . . . . . 8 USGrph 2SPathOnOt
2723, 26bitrd 245 . . . . . . 7 USGrph 2SPathOnOt
2827anbi1d 686 . . . . . 6 USGrph 2SPathOnOt
2928anbi2d 685 . . . . 5 USGrph 2SPathOnOt
30 r19.41vv 23970 . . . . . . 7
31 ancom 438 . . . . . . 7
32 r19.41vv 23970 . . . . . . . 8
3332anbi2i 676 . . . . . . 7
3430, 31, 333bitrri 264 . . . . . 6
35 elsn 3829 . . . . . . . . . . . . 13
3635bicomi 194 . . . . . . . . . . . 12
3736anbi2i 676 . . . . . . . . . . 11
3837anbi2i 676 . . . . . . . . . 10
3938a1i 11 . . . . . . . . 9 USGrph
40 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4140fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
42 vex 2959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
43 vex 2959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
44 vex 2959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
45 ot2ndg 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4642, 43, 44, 45mp3an 1279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
4741, 46syl6eq 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
4847eqeq1d 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
50 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
51 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
5251ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
5349, 50, 523jca 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
54 necom 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
55 df-ne 2601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
5654, 55bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
5756biimpi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
5857ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
5953, 58jca 519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
60 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
61 prcom 3882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
6261eleq1i 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
6362biimpi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
6463adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
6564ad5antlr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
6649, 60, 653jca 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67 simp-5l 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6859, 66, 67jca32 522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6968exp31 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7069exp41 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
72 oteq2 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7372eqeq2d 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
74 preq2 3884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7574eleq1d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
76 preq1 3883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7776eleq1d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7875, 77anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
79 eleq1 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
8079imbi1d 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
8180imbi2d 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8278, 81imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8371, 73, 823imtr4d 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8483com12 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8548, 84sylbid 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8685com24 83 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8786imp31 422 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8887com14 84 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8988adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
9089imp41 577 . . . . . . . . . . . . . . . . . . . . . . . 24
9190com12 29 . . . . . . . . . . . . . . . . . . . . . . 23
92913ad2ant3 980 . . . . . . . . . . . . . . . . . . . . . 22 USGrph
9392exp3acom3r 1379 . . . . . . . . . . . . . . . . . . . . 21 USGrph
9493rexlimdva 2830 . . . . . . . . . . . . . . . . . . . 20 USGrph
9594ex 424 . . . . . . . . . . . . . . . . . . 19 USGrph
9695com13 76 . . . . . . . . . . . . . . . . . 18 USGrph
9796imp 419 . . . . . . . . . . . . . . . . 17 USGrph
9897exp3acom23 1381 . . . . . . . . . . . . . . . 16 USGrph
9998imp 419 . . . . . . . . . . . . . . 15 USGrph
10099exp3acom3r 1379 . . . . . . . . . . . . . 14 USGrph
101100com23 74 . . . . . . . . . . . . 13 USGrph
102101imp 419 . . . . . . . . . . . 12 USGrph
103102impcom 420 . . . . . . . . . . 11 USGrph
104103com12 29 . . . . . . . . . 10 USGrph
105 simprl2 1003 . . . . . . . . . . 11
106 simpll2 997 . . . . . . . . . . 11
107 id 20 . . . . . . . . . . . . . . . . . . . . . 22
108 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10956bicomi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
110109biimpi 187 . . . . . . . . . . . . . . . . . . . . . . . . . 26
111108, 110anim12i 550 . . . . . . . . . . . . . . . . . . . . . . . . 25
112 prcom 3882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
113112eleq1i 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
114113biimpi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
115114anim1i 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
116115ancoms 440 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
117116adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26
118117adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
119111, 118jca 519 . . . . . . . . . . . . . . . . . . . . . . . 24
12073anbi1d 686 . . . . . . . . . . . . . . . . . . . . . . . . 25
121120, 78anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . 24
122119, 121syl5ibr 213 . . . . . . . . . . . . . . . . . . . . . . 23
123122adantl 453 . . . . . . . . . . . . . . . . . . . . . 22
124107, 123rspcimedv 3054 . . . . . . . . . . . . . . . . . . . . 21
125124exp3acom3r 1379 . . . . . . . . . . . . . . . . . . . 20
126125exp31 588 . . . . . . . . . . . . . . . . . . 19
127126com15 89 . . . . . . . . . . . . . . . . . 18
128127imp 419 . . . . . . . . . . . . . . . . 17
1291283adant2 976 . . . . . . . . . . . . . . . 16
130129imp 419 . . . . . . . . . . . . . . 15
131130com13 76 . . . . . . . . . . . . . 14
1321313ad2ant3 980 . . . . . . . . . . . . 13
133132imp31 422 . . . . . . . . . . . 12
134 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . 22
135134fveq2d 5732 . . . . . . . . . . . . . . . . . . . . 21
136 simpl 444 . . . . . . . . . . . . . . . . . . . . . . 23
137 simprl 733 . . . . . . . . . . . . . . . . . . . . . . 23
138 simprr 734 . . . . . . . . . . . . . . . . . . . . . . 23
139136, 137, 1383jca 1134 . . . . . . . . . . . . . . . . . . . . . 22
140 ot2ndg 6362 . . . . . . . . . . . . . . . . . . . . . 22
141139, 140syl 16 . . . . . . . . . . . . . . . . . . . . 21
142135, 141sylan9eqr 2490 . . . . . . . . . . . . . . . . . . . 20
143142exp31 588 . . . . . . . . . . . . . . . . . . 19
144143com23 74 . . . . . . . . . . . . . . . . . 18
1451443ad2ant2 979 . . . . . . . . . . . . . . . . 17
146145imp 419 . . . . . . . . . . . . . . . 16
147146com12 29 . . . . . . . . . . . . . . 15
1481473adant3 977 . . . . . . . . . . . . . 14
149148adantr 452 . . . . . . . . . . . . 13
150149imp 419 . . . . . . . . . . . 12
151 eqidd 2437 . . . . . . . . . . . . . . . . . . . . . . 23
152 otel3xp 28062 . . . . . . . . . . . . . . . . . . . . . . 23
153151, 139, 152syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
154153adantr 452 . . . . . . . . . . . . . . . . . . . . 21
155 eleq1 2496 . . . . . . . . . . . . . . . . . . . . . 22
156155adantl 453 . . . . . . . . . . . . . . . . . . . . 21
157154, 156mpbird 224 . . . . . . . . . . . . . . . . . . . 20
158157exp31 588 . . . . . . . . . . . . . . . . . . 19
159158com23 74 . . . . . . . . . . . . . . . . . 18
1601593ad2ant2 979 . . . . . . . . . . . . . . . . 17
161160imp 419 . . . . . . . . . . . . . . . 16
162161com12 29 . . . . . . . . . . . . . . 15
1631623adant3 977 . . . . . . . . . . . . . 14
164163adantr 452 . . . . . . . . . . . . 13
165164imp 419 . . . . . . . . . . . 12
166133, 150, 165jca31 521 . . . . . . . . . . 11
167105, 106, 166jca32 522 . . . . . . . . . 10
168104, 167impbid1 195 . . . . . . . . 9 USGrph
169 eldif 3330 . . . . . . . . . . 11 Neighbors Neighbors
170 nbgrael 21438 . . . . . . . . . . . . . 14 Neighbors
17120, 170syl 16 . . . . . . . . . . . . 13 USGrph Neighbors
1721713ad2ant1 978 . . . . . . . . . . . 12 USGrph Neighbors
173 elsn 3829 . . . . . . . . . . . . . 14
174173a1i 11 . . . . . . . . . . . . 13 USGrph
175174notbid 286 . . . . . . . . . . . 12 USGrph
176172, 175anbi12d 692 . . . . . . . . . . 11 USGrph Neighbors
177169, 176syl5bb 249 . . . . . . . . . 10 USGrph Neighbors
178 nbgrael 21438 . . . . . . . . . . . . 13 Neighbors
17920, 178syl 16 . . . . . . . . . . . 12 USGrph Neighbors
1801793ad2ant1 978 . . . . . . . . . . 11 USGrph Neighbors
181180anbi1d 686 . . . . . . . . . 10 USGrph Neighbors
182177, 181anbi12d 692 . . . . . . . . 9 USGrph Neighbors Neighbors
18339, 168, 1823bitr4d 277 . . . . . . . 8 USGrph Neighbors Neighbors
1841832exbidv 1638 . . . . . . 7 USGrph Neighbors Neighbors
185 df-rex 2711 . . . . . . . . 9
186185rexbii 2730 . . . . . . . 8
187 df-rex 2711 . . . . . . . 8
188 19.42v 1928 . . . . . . . . . 10
189188bicomi 194 . . . . . . . . 9
190189exbii 1592 . . . . . . . 8
191186, 187, 1903bitri 263 . . . . . . 7
192 df-rex 2711 . . . . . . . 8 Neighbors Neighbors Neighbors Neighbors
193 r19.42v 2862 . . . . . . . . . 10 Neighbors Neighbors Neighbors Neighbors
194 df-rex 2711 . . . . . . . . . 10 Neighbors Neighbors Neighbors Neighbors
195193, 194bitr3i 243 . . . . . . . . 9 Neighbors Neighbors Neighbors Neighbors
196195exbii 1592 . . . . . . . 8 Neighbors Neighbors Neighbors Neighbors
197192, 196bitri 241 . . . . . . 7 Neighbors Neighbors Neighbors Neighbors
198184, 191, 1973bitr4g 280 . . . . . 6 USGrph Neighbors Neighbors
19934, 198syl5bb 249 . . . . 5 USGrph Neighbors Neighbors
20019, 29, 1993bitrd 271 . . . 4 USGrph 2SPathOnOt Neighbors Neighbors
201 vex 2959 . . . . . . 7
202 eleq1 2496 . . . . . . . 8
2032022rexbidv 2748 . . . . . . 7 Neighbors Neighbors Neighbors Neighbors
204201, 203elab 3082 . . . . . 6 Neighbors Neighbors Neighbors Neighbors
205204bicomi 194 . . . . 5 Neighbors Neighbors Neighbors Neighbors
206205a1i 11 . . . 4 USGrph Neighbors Neighbors Neighbors Neighbors
20712, 200, 2063bitrd 271 . . 3 USGrph Neighbors Neighbors
208207eqrdv 2434 . 2 USGrph Neighbors Neighbors
209 dfiunv2 4127 . 2 Neighbors Neighbors Neighbors Neighbors
210208, 209syl6eqr 2486 1 USGrph Neighbors Neighbors
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   w3a 936  wex 1550   wceq 1652   wcel 1725  cab 2422   wne 2599  wrex 2706  crab 2709  cvv 2956   cdif 3317  csn 3814  cpr 3815  cop 3817  cotp 3818  ciun 4093   class class class wbr 4212   cmpt 4266   cxp 4876   crn 4879  cfv 5454  (class class class)co 6081  c1st 6347  c2nd 6348  cfn 7109   USGrph cusg 21365   Neighbors cnbgra 21430   2SPathOnOt c2spthot 28323   2SPathOnOt c2pthonot 28324 This theorem is referenced by:  usgreghash2spotv  28455 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-cnex 9046  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-mulcom 9054  ax-addass 9055  ax-mulass 9056  ax-distr 9057  ax-i2m1 9058  ax-1ne0 9059  ax-1rid 9060  ax-rnegex 9061  ax-rrecex 9062  ax-cnre 9063  ax-pre-lttri 9064  ax-pre-lttrn 9065  ax-pre-ltadd 9066  ax-pre-mulgt0 9067 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-ot 3824  df-uni 4016  df-int 4051  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-1st 6349  df-2nd 6350  df-riota 6549  df-recs 6633  df-rdg 6668  df-1o 6724  df-oadd 6728  df-er 6905  df-map 7020  df-pm 7021  df-en 7110  df-dom 7111  df-sdom 7112  df-fin 7113  df-card 7826  df-cda 8048  df-pnf 9122  df-mnf 9123  df-xr 9124  df-ltxr 9125  df-le 9126  df-sub 9293  df-neg 9294  df-nn 10001  df-2 10058  df-3 10059  df-n0 10222  df-z 10283  df-uz 10489  df-fz 11044  df-fzo 11136  df-hash 11619  df-word 11723  df-usgra 21367  df-nbgra 21433  df-wlk 21516  df-trail 21517  df-pth 21518  df-spth 21519  df-wlkon 21522  df-spthon 21525  df-2wlkonot 28325  df-2spthonot 28327  df-2spthsot 28328
 Copyright terms: Public domain W3C validator