Metamath Proof Explorer


Theorem clwwlknon0

Description: Sufficient conditions for ClWWalksNOn to be empty. (Contributed by AV, 25-Mar-2022)

Ref Expression
Assertion clwwlknon0 ¬ X Vtx G N X ClWWalksNOn G N =

Proof

Step Hyp Ref Expression
1 oveq2 N = 0 X ClWWalksNOn G N = X ClWWalksNOn G 0
2 clwwlk0on0 X ClWWalksNOn G 0 =
3 1 2 eqtrdi N = 0 X ClWWalksNOn G N =
4 3 a1d N = 0 ¬ X Vtx G N X ClWWalksNOn G N =
5 simprl N 0 X Vtx G N 0 X Vtx G
6 elnnne0 N N 0 N 0
7 6 simplbi2 N 0 N 0 N
8 7 adantl X Vtx G N 0 N 0 N
9 8 impcom N 0 X Vtx G N 0 N
10 5 9 jca N 0 X Vtx G N 0 X Vtx G N
11 10 stoic1a N 0 ¬ X Vtx G N ¬ X Vtx G N 0
12 clwwlknonmpo ClWWalksNOn G = v Vtx G , n 0 w n ClWWalksN G | w 0 = v
13 12 mpondm0 ¬ X Vtx G N 0 X ClWWalksNOn G N =
14 11 13 syl N 0 ¬ X Vtx G N X ClWWalksNOn G N =
15 14 ex N 0 ¬ X Vtx G N X ClWWalksNOn G N =
16 4 15 pm2.61ine ¬ X Vtx G N X ClWWalksNOn G N =