Metamath Proof Explorer

Theorem clwwlknon0

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

Ref Expression
Assertion clwwlknon0 
|- ( -. ( X e. ( Vtx ` G ) /\ N e. NN ) -> ( 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 e. ( Vtx ` G ) /\ N e. NN ) -> ( X ( ClWWalksNOn ` G ) N ) = (/) ) )
5 simprl 
 |-  ( ( N =/= 0 /\ ( X e. ( Vtx ` G ) /\ N e. NN0 ) ) -> X e. ( Vtx ` G ) )
6 elnnne0 
 |-  ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
7 6 simplbi2 
 |-  ( N e. NN0 -> ( N =/= 0 -> N e. NN ) )
8 7 adantl 
 |-  ( ( X e. ( Vtx ` G ) /\ N e. NN0 ) -> ( N =/= 0 -> N e. NN ) )
9 8 impcom 
 |-  ( ( N =/= 0 /\ ( X e. ( Vtx ` G ) /\ N e. NN0 ) ) -> N e. NN )
10 5 9 jca 
 |-  ( ( N =/= 0 /\ ( X e. ( Vtx ` G ) /\ N e. NN0 ) ) -> ( X e. ( Vtx ` G ) /\ N e. NN ) )
11 10 stoic1a 
 |-  ( ( N =/= 0 /\ -. ( X e. ( Vtx ` G ) /\ N e. NN ) ) -> -. ( X e. ( Vtx ` G ) /\ N e. NN0 ) )
12 clwwlknonmpo 
 |-  ( ClWWalksNOn ` G ) = ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } )
13 12 mpondm0 
 |-  ( -. ( X e. ( Vtx ` G ) /\ N e. NN0 ) -> ( X ( ClWWalksNOn ` G ) N ) = (/) )
14 11 13 syl 
 |-  ( ( N =/= 0 /\ -. ( X e. ( Vtx ` G ) /\ N e. NN ) ) -> ( X ( ClWWalksNOn ` G ) N ) = (/) )
15 14 ex 
 |-  ( N =/= 0 -> ( -. ( X e. ( Vtx ` G ) /\ N e. NN ) -> ( X ( ClWWalksNOn ` G ) N ) = (/) ) )
16 4 15 pm2.61ine 
 |-  ( -. ( X e. ( Vtx ` G ) /\ N e. NN ) -> ( X ( ClWWalksNOn ` G ) N ) = (/) )