Metamath Proof Explorer


Theorem fusgreg2wsp

Description: In a finite simple graph, the set of all paths of length 2 is the union of all the paths of length 2 over the vertices which are in the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 18-May-2021) (Proof shortened by AV, 10-Jan-2022)

Ref Expression
Hypotheses frgrhash2wsp.v V = Vtx G
fusgreg2wsp.m M = a V w 2 WSPathsN G | w 1 = a
Assertion fusgreg2wsp G FinUSGraph 2 WSPathsN G = x V M x

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v V = Vtx G
2 fusgreg2wsp.m M = a V w 2 WSPathsN G | w 1 = a
3 wspthsswwlkn 2 WSPathsN G 2 WWalksN G
4 3 sseli p 2 WSPathsN G p 2 WWalksN G
5 1 midwwlks2s3 p 2 WWalksN G x V p 1 = x
6 4 5 syl p 2 WSPathsN G x V p 1 = x
7 6 a1i G FinUSGraph p 2 WSPathsN G x V p 1 = x
8 7 pm4.71rd G FinUSGraph p 2 WSPathsN G x V p 1 = x p 2 WSPathsN G
9 ancom p 2 WSPathsN G p 1 = x p 1 = x p 2 WSPathsN G
10 9 rexbii x V p 2 WSPathsN G p 1 = x x V p 1 = x p 2 WSPathsN G
11 r19.41v x V p 1 = x p 2 WSPathsN G x V p 1 = x p 2 WSPathsN G
12 10 11 bitr2i x V p 1 = x p 2 WSPathsN G x V p 2 WSPathsN G p 1 = x
13 12 a1i G FinUSGraph x V p 1 = x p 2 WSPathsN G x V p 2 WSPathsN G p 1 = x
14 1 2 fusgreg2wsplem x V p M x p 2 WSPathsN G p 1 = x
15 14 bicomd x V p 2 WSPathsN G p 1 = x p M x
16 15 adantl G FinUSGraph x V p 2 WSPathsN G p 1 = x p M x
17 16 rexbidva G FinUSGraph x V p 2 WSPathsN G p 1 = x x V p M x
18 8 13 17 3bitrd G FinUSGraph p 2 WSPathsN G x V p M x
19 eliun p x V M x x V p M x
20 18 19 bitr4di G FinUSGraph p 2 WSPathsN G p x V M x
21 20 eqrdv G FinUSGraph 2 WSPathsN G = x V M x