Metamath Proof Explorer


Theorem wlkv0

Description: If there is a walk in the null graph (a class without vertices), it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

Ref Expression
Assertion wlkv0 Vtx G = W Walks G 1 st W = 2 nd W =

Proof

Step Hyp Ref Expression
1 wlkcpr W Walks G 1 st W Walks G 2 nd W
2 eqid iEdg G = iEdg G
3 2 wlkf 1 st W Walks G 2 nd W 1 st W Word dom iEdg G
4 eqid Vtx G = Vtx G
5 4 wlkp 1 st W Walks G 2 nd W 2 nd W : 0 1 st W Vtx G
6 3 5 jca 1 st W Walks G 2 nd W 1 st W Word dom iEdg G 2 nd W : 0 1 st W Vtx G
7 feq3 Vtx G = 2 nd W : 0 1 st W Vtx G 2 nd W : 0 1 st W
8 f00 2 nd W : 0 1 st W 2 nd W = 0 1 st W =
9 7 8 bitrdi Vtx G = 2 nd W : 0 1 st W Vtx G 2 nd W = 0 1 st W =
10 0z 0
11 nn0z 1 st W 0 1 st W
12 fzn 0 1 st W 1 st W < 0 0 1 st W =
13 10 11 12 sylancr 1 st W 0 1 st W < 0 0 1 st W =
14 nn0nlt0 1 st W 0 ¬ 1 st W < 0
15 14 pm2.21d 1 st W 0 1 st W < 0 1 st W =
16 13 15 sylbird 1 st W 0 0 1 st W = 1 st W =
17 16 com12 0 1 st W = 1 st W 0 1 st W =
18 17 adantl 2 nd W = 0 1 st W = 1 st W 0 1 st W =
19 lencl 1 st W Word dom iEdg G 1 st W 0
20 18 19 impel 2 nd W = 0 1 st W = 1 st W Word dom iEdg G 1 st W =
21 simpll 2 nd W = 0 1 st W = 1 st W Word dom iEdg G 2 nd W =
22 20 21 jca 2 nd W = 0 1 st W = 1 st W Word dom iEdg G 1 st W = 2 nd W =
23 22 ex 2 nd W = 0 1 st W = 1 st W Word dom iEdg G 1 st W = 2 nd W =
24 9 23 syl6bi Vtx G = 2 nd W : 0 1 st W Vtx G 1 st W Word dom iEdg G 1 st W = 2 nd W =
25 24 impcomd Vtx G = 1 st W Word dom iEdg G 2 nd W : 0 1 st W Vtx G 1 st W = 2 nd W =
26 6 25 syl5 Vtx G = 1 st W Walks G 2 nd W 1 st W = 2 nd W =
27 1 26 syl5bi Vtx G = W Walks G 1 st W = 2 nd W =
28 27 imp Vtx G = W Walks G 1 st W = 2 nd W =