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 VtxG=WWalksG1stW=2ndW=

Proof

Step Hyp Ref Expression
1 wlkcpr WWalksG1stWWalksG2ndW
2 eqid iEdgG=iEdgG
3 2 wlkf 1stWWalksG2ndW1stWWorddomiEdgG
4 eqid VtxG=VtxG
5 4 wlkp 1stWWalksG2ndW2ndW:01stWVtxG
6 3 5 jca 1stWWalksG2ndW1stWWorddomiEdgG2ndW:01stWVtxG
7 feq3 VtxG=2ndW:01stWVtxG2ndW:01stW
8 f00 2ndW:01stW2ndW=01stW=
9 7 8 bitrdi VtxG=2ndW:01stWVtxG2ndW=01stW=
10 0z 0
11 nn0z 1stW01stW
12 fzn 01stW1stW<001stW=
13 10 11 12 sylancr 1stW01stW<001stW=
14 nn0nlt0 1stW0¬1stW<0
15 14 pm2.21d 1stW01stW<01stW=
16 13 15 sylbird 1stW001stW=1stW=
17 16 com12 01stW=1stW01stW=
18 17 adantl 2ndW=01stW=1stW01stW=
19 lencl 1stWWorddomiEdgG1stW0
20 18 19 impel 2ndW=01stW=1stWWorddomiEdgG1stW=
21 simpll 2ndW=01stW=1stWWorddomiEdgG2ndW=
22 20 21 jca 2ndW=01stW=1stWWorddomiEdgG1stW=2ndW=
23 22 ex 2ndW=01stW=1stWWorddomiEdgG1stW=2ndW=
24 9 23 syl6bi VtxG=2ndW:01stWVtxG1stWWorddomiEdgG1stW=2ndW=
25 24 impcomd VtxG=1stWWorddomiEdgG2ndW:01stWVtxG1stW=2ndW=
26 6 25 syl5 VtxG=1stWWalksG2ndW1stW=2ndW=
27 1 26 biimtrid VtxG=WWalksG1stW=2ndW=
28 27 imp VtxG=WWalksG1stW=2ndW=