Theorem clwwlknon0

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

	Ref	Expression
Assertion	clwwlknon0	⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑁 = 0 → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 0 ) )
2		clwwlk0on0	⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 0 ) = ∅
3	1 2	eqtrdi	⊢ ( 𝑁 = 0 → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ∅ )
4	3	a1d	⊢ ( 𝑁 = 0 → ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ∅ ) )
5		simprl	⊢ ( ( 𝑁 ≠ 0 ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) ) → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
6		elnnne0	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
7	6	simplbi2	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≠ 0 → 𝑁 ∈ ℕ ) )
8	7	adantl	⊢ ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ≠ 0 → 𝑁 ∈ ℕ ) )
9	8	impcom	⊢ ( ( 𝑁 ≠ 0 ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ )
10	5 9	jca	⊢ ( ( 𝑁 ≠ 0 ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ) )
11	10	stoic1a	⊢ ( ( 𝑁 ≠ 0 ∧ ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ) ) → ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) )
12		clwwlknonmpo	⊢ ( ClWWalksNOn ‘ 𝐺 ) = ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } )
13	12	mpondm0	⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ∅ )
14	11 13	syl	⊢ ( ( 𝑁 ≠ 0 ∧ ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ∅ )
15	14	ex	⊢ ( 𝑁 ≠ 0 → ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ∅ ) )
16	4 15	pm2.61ine	⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ∅ )