Metamath Proof Explorer


Theorem wlkson

Description: The set of walks between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017) (Revised by AV, 30-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypothesis wlkson.v V = Vtx G
Assertion wlkson A V B V A WalksOn G B = f p | f Walks G p p 0 = A p f = B

Proof

Step Hyp Ref Expression
1 wlkson.v V = Vtx G
2 1 1vgrex A V G V
3 2 adantr A V B V G V
4 simpl A V B V A V
5 4 1 eleqtrdi A V B V A Vtx G
6 simpr A V B V B V
7 6 1 eleqtrdi A V B V B Vtx G
8 wksv f p | f Walks G p V
9 8 a1i A V B V f p | f Walks G p V
10 simpr A V B V f Walks G p f Walks G p
11 eqeq2 a = A p 0 = a p 0 = A
12 eqeq2 b = B p f = b p f = B
13 11 12 bi2anan9 a = A b = B p 0 = a p f = b p 0 = A p f = B
14 biidd g = G p 0 = a p f = b p 0 = a p f = b
15 df-wlkson WalksOn = g V a Vtx g , b Vtx g f p | f Walks g p p 0 = a p f = b
16 eqid Vtx g = Vtx g
17 3anass f Walks g p p 0 = a p f = b f Walks g p p 0 = a p f = b
18 17 biancomi f Walks g p p 0 = a p f = b p 0 = a p f = b f Walks g p
19 18 opabbii f p | f Walks g p p 0 = a p f = b = f p | p 0 = a p f = b f Walks g p
20 16 16 19 mpoeq123i a Vtx g , b Vtx g f p | f Walks g p p 0 = a p f = b = a Vtx g , b Vtx g f p | p 0 = a p f = b f Walks g p
21 20 mpteq2i g V a Vtx g , b Vtx g f p | f Walks g p p 0 = a p f = b = g V a Vtx g , b Vtx g f p | p 0 = a p f = b f Walks g p
22 15 21 eqtri WalksOn = g V a Vtx g , b Vtx g f p | p 0 = a p f = b f Walks g p
23 3 5 7 9 10 13 14 22 mptmpoopabbrd A V B V A WalksOn G B = f p | p 0 = A p f = B f Walks G p
24 ancom p 0 = A p f = B f Walks G p f Walks G p p 0 = A p f = B
25 3anass f Walks G p p 0 = A p f = B f Walks G p p 0 = A p f = B
26 24 25 bitr4i p 0 = A p f = B f Walks G p f Walks G p p 0 = A p f = B
27 26 opabbii f p | p 0 = A p f = B f Walks G p = f p | f Walks G p p 0 = A p f = B
28 23 27 eqtrdi A V B V A WalksOn G B = f p | f Walks G p p 0 = A p f = B