Metamath Proof Explorer


Theorem wspthsnon

Description: The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 11-May-2021)

Ref Expression
Hypothesis wwlksnon.v V = Vtx G
Assertion wspthsnon N 0 G U N WSPathsNOn G = a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w

Proof

Step Hyp Ref Expression
1 wwlksnon.v V = Vtx G
2 df-wspthsnon WSPathsNOn = n 0 , g V a Vtx g , b Vtx g w a n WWalksNOn g b | f f a SPathsOn g b w
3 2 a1i N 0 G U WSPathsNOn = n 0 , g V a Vtx g , b Vtx g w a n WWalksNOn g b | f f a SPathsOn g b w
4 fveq2 g = G Vtx g = Vtx G
5 4 1 eqtr4di g = G Vtx g = V
6 5 adantl n = N g = G Vtx g = V
7 oveq12 n = N g = G n WWalksNOn g = N WWalksNOn G
8 7 oveqd n = N g = G a n WWalksNOn g b = a N WWalksNOn G b
9 fveq2 g = G SPathsOn g = SPathsOn G
10 9 oveqd g = G a SPathsOn g b = a SPathsOn G b
11 10 breqd g = G f a SPathsOn g b w f a SPathsOn G b w
12 11 adantl n = N g = G f a SPathsOn g b w f a SPathsOn G b w
13 12 exbidv n = N g = G f f a SPathsOn g b w f f a SPathsOn G b w
14 8 13 rabeqbidv n = N g = G w a n WWalksNOn g b | f f a SPathsOn g b w = w a N WWalksNOn G b | f f a SPathsOn G b w
15 6 6 14 mpoeq123dv n = N g = G a Vtx g , b Vtx g w a n WWalksNOn g b | f f a SPathsOn g b w = a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w
16 15 adantl N 0 G U n = N g = G a Vtx g , b Vtx g w a n WWalksNOn g b | f f a SPathsOn g b w = a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w
17 simpl N 0 G U N 0
18 elex G U G V
19 18 adantl N 0 G U G V
20 1 fvexi V V
21 20 20 mpoex a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w V
22 21 a1i N 0 G U a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w V
23 3 16 17 19 22 ovmpod N 0 G U N WSPathsNOn G = a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w