Theorem wwlksnndef

Description: Conditions for WWalksN not being defined. (Contributed by Alexander van der Vekens, 30-Jul-2018) (Revised by AV, 19-Apr-2021)

	Ref	Expression
Assertion	wwlksnndef	⊢ ( ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ0 ) → ( 𝑁 WWalksN 𝐺 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		neq0	⊢ ( ¬ ( 𝑁 WWalksN 𝐺 ) = ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) )
2		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3	2	wwlknbp	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ) )
4		nnel	⊢ ( ¬ 𝐺 ∉ V ↔ 𝐺 ∈ V )
5		nnel	⊢ ( ¬ 𝑁 ∉ ℕ0 ↔ 𝑁 ∈ ℕ0 )
6	4 5	anbi12i	⊢ ( ( ¬ 𝐺 ∉ V ∧ ¬ 𝑁 ∉ ℕ0 ) ↔ ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ) )
7	6	biimpri	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ) → ( ¬ 𝐺 ∉ V ∧ ¬ 𝑁 ∉ ℕ0 ) )
8	7	3adant3	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ¬ 𝐺 ∉ V ∧ ¬ 𝑁 ∉ ℕ0 ) )
9		ioran	⊢ ( ¬ ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ0 ) ↔ ( ¬ 𝐺 ∉ V ∧ ¬ 𝑁 ∉ ℕ0 ) )
10	8 9	sylibr	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ) → ¬ ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ0 ) )
11	3 10	syl	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ¬ ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ0 ) )
12	11	exlimiv	⊢ ( ∃ 𝑤 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ¬ ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ0 ) )
13	1 12	sylbi	⊢ ( ¬ ( 𝑁 WWalksN 𝐺 ) = ∅ → ¬ ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ0 ) )
14	13	con4i	⊢ ( ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ0 ) → ( 𝑁 WWalksN 𝐺 ) = ∅ )