Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  usg2spot2nb Structured version   Visualization version   Unicode version

Theorem usg2spot2nb 25872
 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 1032 . . . . 5 USGrph
2 3xpexg 6613 . . . . . . 7
3 rabexg 4549 . . . . . . 7 2SPathOnOt
42, 3syl 17 . . . . . 6 2SPathOnOt
543ad2ant2 1052 . . . . 5 USGrph 2SPathOnOt
6 eqeq2 2482 . . . . . . . . 9
76anbi2d 718 . . . . . . . 8 2SPathOnOt 2SPathOnOt
87rabbidv 3022 . . . . . . 7 2SPathOnOt 2SPathOnOt
9 usgreghash2spot.m . . . . . . 7 2SPathOnOt
108, 9fvmptg 5961 . . . . . 6 2SPathOnOt 2SPathOnOt
1110eleq2d 2534 . . . . 5 2SPathOnOt 2SPathOnOt
121, 5, 11syl2anc 673 . . . 4 USGrph 2SPathOnOt
13 eleq1 2537 . . . . . . . 8 2SPathOnOt 2SPathOnOt
14 fveq2 5879 . . . . . . . . . 10
1514fveq2d 5883 . . . . . . . . 9
1615eqeq1d 2473 . . . . . . . 8
1713, 16anbi12d 725 . . . . . . 7 2SPathOnOt 2SPathOnOt
1817elrab 3184 . . . . . 6 2SPathOnOt 2SPathOnOt
1918a1i 11 . . . . 5 USGrph 2SPathOnOt 2SPathOnOt
20 usgrav 25144 . . . . . . . . . 10 USGrph
21 el2spthsoton 25686 . . . . . . . . . 10 2SPathOnOt 2SPathOnOt
2220, 21syl 17 . . . . . . . . 9 USGrph 2SPathOnOt 2SPathOnOt
23223ad2ant1 1051 . . . . . . . 8 USGrph 2SPathOnOt 2SPathOnOt
24 usg2spthonot1 25697 . . . . . . . . . 10 USGrph 2SPathOnOt
25243ad2antl1 1192 . . . . . . . . 9 USGrph 2SPathOnOt
26252rexbidva 2896 . . . . . . . 8 USGrph 2SPathOnOt
2723, 26bitrd 261 . . . . . . 7 USGrph 2SPathOnOt
2827anbi1d 719 . . . . . 6 USGrph 2SPathOnOt
2928anbi2d 718 . . . . 5 USGrph 2SPathOnOt
30 r19.41vv 2930 . . . . . . 7
31 ancom 457 . . . . . . 7
32 r19.41vv 2930 . . . . . . . 8
3332anbi2i 708 . . . . . . 7
3430, 31, 333bitrri 280 . . . . . 6
35 elsn 3973 . . . . . . . . . . . . 13
3635bicomi 207 . . . . . . . . . . . 12
3736anbi2i 708 . . . . . . . . . . 11
3837anbi2i 708 . . . . . . . . . 10
3938a1i 11 . . . . . . . . 9 USGrph
40 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4140fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
42 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
43 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
44 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
45 ot2ndg 6827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4642, 43, 44, 45mp3an 1390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
4741, 46syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
4847eqeq1d 2473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
50 simplrl 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
51 simplrr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
5251ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
5349, 50, 523jca 1210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
54 nesym 2699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
5554biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
5655ad4antlr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
5753, 56jca 541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58 simplrr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
59 prcom 4041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
6059eleq1i 2540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
6160biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
6261adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
6362ad5antlr 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
6449, 58, 633jca 1210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
65 simp-5l 786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6657, 64, 65jca32 544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6766exp31 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6867exp41 621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6968a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
70 oteq2 4168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7170eqeq2d 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
72 preq2 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7372eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
74 preq1 4042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7574eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7673, 75anbi12d 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
77 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7877imbi1d 324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7978imbi2d 323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8076, 79imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8169, 71, 803imtr4d 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8281com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8348, 82sylbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8483com24 89 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8584imp31 439 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8685com14 90 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8786adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
8887imp41 604 . . . . . . . . . . . . . . . . . . . . . . . 24
8988com12 31 . . . . . . . . . . . . . . . . . . . . . . 23
90893ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . 22 USGrph
9190expdcom 446 . . . . . . . . . . . . . . . . . . . . 21 USGrph
9291rexlimdva 2871 . . . . . . . . . . . . . . . . . . . 20 USGrph
9392ex 441 . . . . . . . . . . . . . . . . . . 19 USGrph
9493com13 82 . . . . . . . . . . . . . . . . . 18 USGrph
9594imp 436 . . . . . . . . . . . . . . . . 17 USGrph
9695expcomd 445 . . . . . . . . . . . . . . . 16 USGrph
9796imp 436 . . . . . . . . . . . . . . 15 USGrph
9897expdcom 446 . . . . . . . . . . . . . 14 USGrph
9998com23 80 . . . . . . . . . . . . 13 USGrph
10099imp 436 . . . . . . . . . . . 12 USGrph
101100impcom 437 . . . . . . . . . . 11 USGrph
102101com12 31 . . . . . . . . . 10 USGrph
103 simprl2 1076 . . . . . . . . . . 11
104 simpll2 1070 . . . . . . . . . . 11
105 id 22 . . . . . . . . . . . . . . . . . . . . . 22
106 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10754bicomi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
108107biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . 26
109106, 108anim12i 576 . . . . . . . . . . . . . . . . . . . . . . . . 25
110 prcom 4041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111110eleq1i 2540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112111biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
113112anim1i 578 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
114113ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
115114adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
116115adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
117109, 116jca 541 . . . . . . . . . . . . . . . . . . . . . . . 24
11871anbi1d 719 . . . . . . . . . . . . . . . . . . . . . . . . 25
119118, 76anbi12d 725 . . . . . . . . . . . . . . . . . . . . . . . 24
120117, 119syl5ibr 229 . . . . . . . . . . . . . . . . . . . . . . 23
121120adantl 473 . . . . . . . . . . . . . . . . . . . . . 22
122105, 121rspcimedv 3138 . . . . . . . . . . . . . . . . . . . . 21
123122expdcom 446 . . . . . . . . . . . . . . . . . . . 20
124123exp31 615 . . . . . . . . . . . . . . . . . . 19
125124com15 95 . . . . . . . . . . . . . . . . . 18
126125imp 436 . . . . . . . . . . . . . . . . 17
1271263adant2 1049 . . . . . . . . . . . . . . . 16
128127imp 436 . . . . . . . . . . . . . . 15
129128com13 82 . . . . . . . . . . . . . 14
1301293ad2ant3 1053 . . . . . . . . . . . . 13
131130imp31 439 . . . . . . . . . . . 12
132 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22
133132fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21
134 simpl 464 . . . . . . . . . . . . . . . . . . . . . . 23
135 simprl 772 . . . . . . . . . . . . . . . . . . . . . . 23
136 simprr 774 . . . . . . . . . . . . . . . . . . . . . . 23
137134, 135, 1363jca 1210 . . . . . . . . . . . . . . . . . . . . . 22
138 ot2ndg 6827 . . . . . . . . . . . . . . . . . . . . . 22
139137, 138syl 17 . . . . . . . . . . . . . . . . . . . . 21
140133, 139sylan9eqr 2527 . . . . . . . . . . . . . . . . . . . 20
141140exp31 615 . . . . . . . . . . . . . . . . . . 19
142141com23 80 . . . . . . . . . . . . . . . . . 18
1431423ad2ant2 1052 . . . . . . . . . . . . . . . . 17
144143imp 436 . . . . . . . . . . . . . . . 16
145144com12 31 . . . . . . . . . . . . . . 15
1461453adant3 1050 . . . . . . . . . . . . . 14
147146adantr 472 . . . . . . . . . . . . 13
148147imp 436 . . . . . . . . . . . 12
149 eqidd 2472 . . . . . . . . . . . . . . . . . . . . . . 23
150 otel3xp 4875 . . . . . . . . . . . . . . . . . . . . . . 23
151149, 137, 150syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
152151adantr 472 . . . . . . . . . . . . . . . . . . . . 21
153 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . 22
154153adantl 473 . . . . . . . . . . . . . . . . . . . . 21
155152, 154mpbird 240 . . . . . . . . . . . . . . . . . . . 20
156155exp31 615 . . . . . . . . . . . . . . . . . . 19
157156com23 80 . . . . . . . . . . . . . . . . . 18
1581573ad2ant2 1052 . . . . . . . . . . . . . . . . 17
159158imp 436 . . . . . . . . . . . . . . . 16
160159com12 31 . . . . . . . . . . . . . . 15
1611603adant3 1050 . . . . . . . . . . . . . 14
162161adantr 472 . . . . . . . . . . . . 13
163162imp 436 . . . . . . . . . . . 12
164131, 148, 163jca31 543 . . . . . . . . . . 11
165103, 104, 164jca32 544 . . . . . . . . . 10
166102, 165impbid1 208 . . . . . . . . 9 USGrph
167 eldif 3400 . . . . . . . . . . 11 Neighbors Neighbors
168 nbgrael 25233 . . . . . . . . . . . . . 14 Neighbors
16920, 168syl 17 . . . . . . . . . . . . 13 USGrph Neighbors
1701693ad2ant1 1051 . . . . . . . . . . . 12 USGrph Neighbors
171 elsn 3973 . . . . . . . . . . . . . 14
172171a1i 11 . . . . . . . . . . . . 13 USGrph
173172notbid 301 . . . . . . . . . . . 12 USGrph
174170, 173anbi12d 725 . . . . . . . . . . 11 USGrph Neighbors
175167, 174syl5bb 265 . . . . . . . . . 10 USGrph Neighbors
176 nbgrael 25233 . . . . . . . . . . . . 13 Neighbors
17720, 176syl 17 . . . . . . . . . . . 12 USGrph Neighbors
1781773ad2ant1 1051 . . . . . . . . . . 11 USGrph Neighbors
179178anbi1d 719 . . . . . . . . . 10 USGrph Neighbors
180175, 179anbi12d 725 . . . . . . . . 9 USGrph Neighbors Neighbors
18139, 166, 1803bitr4d 293 . . . . . . . 8 USGrph Neighbors Neighbors
1821812exbidv 1778 . . . . . . 7 USGrph Neighbors Neighbors
183 df-rex 2762 . . . . . . . . 9
184183rexbii 2881 . . . . . . . 8
185 df-rex 2762 . . . . . . . 8
186 19.42v 1842 . . . . . . . . . 10
187186bicomi 207 . . . . . . . . 9
188187exbii 1726 . . . . . . . 8
189184, 185, 1883bitri 279 . . . . . . 7
190 df-rex 2762 . . . . . . . 8 Neighbors Neighbors Neighbors Neighbors
191 r19.42v 2931 . . . . . . . . . 10 Neighbors Neighbors Neighbors Neighbors
192 df-rex 2762 . . . . . . . . . 10 Neighbors Neighbors Neighbors Neighbors
193191, 192bitr3i 259 . . . . . . . . 9 Neighbors Neighbors Neighbors Neighbors
194193exbii 1726 . . . . . . . 8 Neighbors Neighbors Neighbors Neighbors
195190, 194bitri 257 . . . . . . 7 Neighbors Neighbors Neighbors Neighbors
196182, 189, 1953bitr4g 296 . . . . . 6 USGrph Neighbors Neighbors
19734, 196syl5bb 265 . . . . 5 USGrph Neighbors Neighbors
19819, 29, 1973bitrd 287 . . . 4 USGrph 2SPathOnOt Neighbors Neighbors
199 vex 3034 . . . . . . 7
200 eleq1 2537 . . . . . . . 8
2012002rexbidv 2897 . . . . . . 7 Neighbors Neighbors Neighbors Neighbors
202199, 201elab 3173 . . . . . 6 Neighbors Neighbors Neighbors Neighbors
203202bicomi 207 . . . . 5 Neighbors Neighbors Neighbors Neighbors
204203a1i 11 . . . 4 USGrph Neighbors Neighbors Neighbors Neighbors
20512, 198, 2043bitrd 287 . . 3 USGrph Neighbors Neighbors
206205eqrdv 2469 . 2 USGrph Neighbors Neighbors
207 dfiunv2 4305 . 2 Neighbors Neighbors Neighbors Neighbors
208206, 207syl6eqr 2523 1 USGrph Neighbors Neighbors
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904  cab 2457   wne 2641  wrex 2757  crab 2760  cvv 3031   cdif 3387  csn 3959  cpr 3961  cop 3965  cotp 3967  ciun 4269   class class class wbr 4395   cmpt 4454   cxp 4837   crn 4840  cfv 5589  (class class class)co 6308  c1st 6810  c2nd 6811  cfn 7587   USGrph cusg 25136   Neighbors cnbgra 25224   2SPathOnOt c2spthot 25663   2SPathOnOt c2pthonot 25664 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-ot 3968  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-2 10690  df-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-fzo 11943  df-hash 12554  df-word 12711  df-usgra 25139  df-nbgra 25227  df-wlk 25315  df-trail 25316  df-pth 25317  df-spth 25318  df-wlkon 25321  df-spthon 25324  df-2wlkonot 25665  df-2spthonot 25667  df-2spthsot 25668 This theorem is referenced by:  usgreghash2spotv  25873
 Copyright terms: Public domain W3C validator