Metamath Proof Explorer


Theorem clwwlknon0

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

Ref Expression
Assertion clwwlknon0 ¬XVtxGNXClWWalksNOnGN=

Proof

Step Hyp Ref Expression
1 oveq2 N=0XClWWalksNOnGN=XClWWalksNOnG0
2 clwwlk0on0 XClWWalksNOnG0=
3 1 2 eqtrdi N=0XClWWalksNOnGN=
4 3 a1d N=0¬XVtxGNXClWWalksNOnGN=
5 simprl N0XVtxGN0XVtxG
6 elnnne0 NN0N0
7 6 simplbi2 N0N0N
8 7 adantl XVtxGN0N0N
9 8 impcom N0XVtxGN0N
10 5 9 jca N0XVtxGN0XVtxGN
11 10 stoic1a N0¬XVtxGN¬XVtxGN0
12 clwwlknonmpo ClWWalksNOnG=vVtxG,n0wnClWWalksNG|w0=v
13 12 mpondm0 ¬XVtxGN0XClWWalksNOnGN=
14 11 13 syl N0¬XVtxGNXClWWalksNOnGN=
15 14 ex N0¬XVtxGNXClWWalksNOnGN=
16 4 15 pm2.61ine ¬XVtxGNXClWWalksNOnGN=