Metamath Proof Explorer


Theorem g0wlk0

Description: There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

Ref Expression
Assertion g0wlk0 Vtx G = Walks G =

Proof

Step Hyp Ref Expression
1 ax-1 Walks G = Vtx G = Walks G =
2 neq0 ¬ Walks G = w w Walks G
3 wlkv0 Vtx G = w Walks G 1 st w = 2 nd w =
4 wlkcpr w Walks G 1 st w Walks G 2 nd w
5 wlkn0 1 st w Walks G 2 nd w 2 nd w
6 eqneqall 2 nd w = 2 nd w Walks G =
7 6 adantl 1 st w = 2 nd w = 2 nd w Walks G =
8 5 7 syl5com 1 st w Walks G 2 nd w 1 st w = 2 nd w = Walks G =
9 4 8 sylbi w Walks G 1 st w = 2 nd w = Walks G =
10 9 adantl Vtx G = w Walks G 1 st w = 2 nd w = Walks G =
11 3 10 mpd Vtx G = w Walks G Walks G =
12 11 expcom w Walks G Vtx G = Walks G =
13 12 exlimiv w w Walks G Vtx G = Walks G =
14 2 13 sylbi ¬ Walks G = Vtx G = Walks G =
15 1 14 pm2.61i Vtx G = Walks G =