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 ⊢ G ∉ V ∨ N ∉ ℕ 0 → N WWalksN G = ∅

Proof

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