This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐺 ) = ∅ )