Metamath Proof Explorer


Theorem iswspthsnon

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, 12-May-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypothesis iswspthsnon.v V = Vtx G
Assertion iswspthsnon A N WSPathsNOn G B = w A N WWalksNOn G B | f f A SPathsOn G B w

Proof

Step Hyp Ref Expression
1 iswspthsnon.v V = Vtx G
2 0ov A B =
3 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
4 3 mpondm0 ¬ N 0 G V N WSPathsNOn G =
5 4 oveqd ¬ N 0 G V A N WSPathsNOn G B = A B
6 id ¬ N 0 G V ¬ N 0 G V
7 6 intnanrd ¬ N 0 G V ¬ N 0 G V A V B V
8 1 wwlksnon0 ¬ N 0 G V A V B V A N WWalksNOn G B =
9 7 8 syl ¬ N 0 G V A N WWalksNOn G B =
10 9 rabeqdv ¬ N 0 G V w A N WWalksNOn G B | f f A SPathsOn G B w = w | f f A SPathsOn G B w
11 rab0 w | f f A SPathsOn G B w =
12 10 11 eqtrdi ¬ N 0 G V w A N WWalksNOn G B | f f A SPathsOn G B w =
13 2 5 12 3eqtr4a ¬ N 0 G V A N WSPathsNOn G B = w A N WWalksNOn G B | f f A SPathsOn G B w
14 1 wspthsnon N 0 G V N WSPathsNOn G = a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w
15 14 adantr N 0 G V ¬ A V B V N WSPathsNOn G = a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w
16 15 oveqd N 0 G V ¬ A V B V A N WSPathsNOn G B = A a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w B
17 eqid a V , b V 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
18 17 mpondm0 ¬ A V B V A a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w B =
19 18 adantl N 0 G V ¬ A V B V A a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w B =
20 16 19 eqtrd N 0 G V ¬ A V B V A N WSPathsNOn G B =
21 20 ex N 0 G V ¬ A V B V A N WSPathsNOn G B =
22 5 2 eqtrdi ¬ N 0 G V A N WSPathsNOn G B =
23 22 a1d ¬ N 0 G V ¬ A V B V A N WSPathsNOn G B =
24 21 23 pm2.61i ¬ A V B V A N WSPathsNOn G B =
25 1 wwlksonvtx w A N WWalksNOn G B A V B V
26 25 pm2.24d w A N WWalksNOn G B ¬ A V B V ¬ f A SPathsOn G B w
27 26 impcom ¬ A V B V w A N WWalksNOn G B ¬ f A SPathsOn G B w
28 27 nexdv ¬ A V B V w A N WWalksNOn G B ¬ f f A SPathsOn G B w
29 28 ralrimiva ¬ A V B V w A N WWalksNOn G B ¬ f f A SPathsOn G B w
30 rabeq0 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
31 29 30 sylibr ¬ A V B V w A N WWalksNOn G B | f f A SPathsOn G B w =
32 24 31 eqtr4d ¬ A V B V A N WSPathsNOn G B = w A N WWalksNOn G B | f f A SPathsOn G B w
33 14 adantr N 0 G V A V B V N WSPathsNOn G = a V , b V w a N WWalksNOn G b | f f a SPathsOn G b w
34 oveq12 a = A b = B a N WWalksNOn G b = A N WWalksNOn G B
35 oveq12 a = A b = B a SPathsOn G b = A SPathsOn G B
36 35 breqd a = A b = B f a SPathsOn G b w f A SPathsOn G B w
37 36 exbidv a = A b = B f f a SPathsOn G b w f f A SPathsOn G B w
38 34 37 rabeqbidv a = A b = B 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
39 38 adantl N 0 G V A V B V a = A b = B 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
40 simprl N 0 G V A V B V A V
41 simprr N 0 G V A V B V B V
42 ovex A N WWalksNOn G B V
43 42 rabex w A N WWalksNOn G B | f f A SPathsOn G B w V
44 43 a1i N 0 G V A V B V w A N WWalksNOn G B | f f A SPathsOn G B w V
45 33 39 40 41 44 ovmpod N 0 G V A V B V A N WSPathsNOn G B = w A N WWalksNOn G B | f f A SPathsOn G B w
46 13 32 45 ecase A N WSPathsNOn G B = w A N WWalksNOn G B | f f A SPathsOn G B w