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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wlkcpr | |
|
2 | eqid | |
|
3 | 2 | wlkf | |
4 | eqid | |
|
5 | 4 | wlkp | |
6 | 3 5 | jca | |
7 | feq3 | |
|
8 | f00 | |
|
9 | 7 8 | bitrdi | |
10 | 0z | |
|
11 | nn0z | |
|
12 | fzn | |
|
13 | 10 11 12 | sylancr | |
14 | nn0nlt0 | |
|
15 | 14 | pm2.21d | |
16 | 13 15 | sylbird | |
17 | 16 | com12 | |
18 | 17 | adantl | |
19 | lencl | |
|
20 | 18 19 | impel | |
21 | simpll | |
|
22 | 20 21 | jca | |
23 | 22 | ex | |
24 | 9 23 | syl6bi | |
25 | 24 | impcomd | |
26 | 6 25 | syl5 | |
27 | 1 26 | biimtrid | |
28 | 27 | imp | |