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 e. V |-> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } )
Assertion	fusgreg2wsp	|- ( G e. FinUSGraph -> ( 2 WSPathsN G ) = U_ x e. V ( M ` x ) )

Proof

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