Metamath Proof Explorer


Theorem clwwlkneq0

Description: Sufficient conditions for ClWWalksN to be empty. (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 24-Apr-2021) (Proof shortened by AV, 24-Feb-2022)

Ref Expression
Assertion clwwlkneq0 G V N N ClWWalksN G =

Proof

Step Hyp Ref Expression
1 df-nel G V ¬ G V
2 ianor ¬ N 0 N 0 ¬ N 0 ¬ N 0
3 1 2 orbi12i G V ¬ N 0 N 0 ¬ G V ¬ N 0 ¬ N 0
4 df-nel N ¬ N
5 elnnne0 N N 0 N 0
6 4 5 xchbinx N ¬ N 0 N 0
7 6 orbi2i G V N G V ¬ N 0 N 0
8 orass ¬ G V ¬ N 0 ¬ N 0 ¬ G V ¬ N 0 ¬ N 0
9 3 7 8 3bitr4i G V N ¬ G V ¬ N 0 ¬ N 0
10 ianor ¬ N 0 G V ¬ N 0 ¬ G V
11 orcom ¬ N 0 ¬ G V ¬ G V ¬ N 0
12 10 11 bitri ¬ N 0 G V ¬ G V ¬ N 0
13 df-clwwlkn ClWWalksN = n 0 , g V w ClWWalks g | w = n
14 13 mpondm0 ¬ N 0 G V N ClWWalksN G =
15 12 14 sylbir ¬ G V ¬ N 0 N ClWWalksN G =
16 nne ¬ N 0 N = 0
17 oveq1 N = 0 N ClWWalksN G = 0 ClWWalksN G
18 clwwlkn0 0 ClWWalksN G =
19 17 18 eqtrdi N = 0 N ClWWalksN G =
20 16 19 sylbi ¬ N 0 N ClWWalksN G =
21 15 20 jaoi ¬ G V ¬ N 0 ¬ N 0 N ClWWalksN G =
22 9 21 sylbi G V N N ClWWalksN G =