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

Metamath Proof Explorer

Theorem clwwlkneq0

Description: Sufficient conditions for ClWWalksN to be empty. (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 24-Apr-2021) (Proof shortened by AV, 24-Feb-2022)

Ref Expression
Assertion clwwlkneq0 ( ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ ) → ( 𝑁 ClWWalksN 𝐺 ) = ∅ )

Proof

Step Hyp Ref Expression
1 df-nel ⊢ ( 𝐺 ∉ V ↔ ¬ 𝐺 ∈ V )
2 ianor ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) ↔ ( ¬ 𝑁 ∈ ℕ0 ∨ ¬ 𝑁 ≠ 0 ) )
3 1 2 orbi12i ⊢ ( ( 𝐺 ∉ V ∨ ¬ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) ) ↔ ( ¬ 𝐺 ∈ V ∨ ( ¬ 𝑁 ∈ ℕ0 ∨ ¬ 𝑁 ≠ 0 ) ) )
4 df-nel ⊢ ( 𝑁 ∉ ℕ ↔ ¬ 𝑁 ∈ ℕ )
5 elnnne0 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
6 4 5 xchbinx ⊢ ( 𝑁 ∉ ℕ ↔ ¬ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
7 6 orbi2i ⊢ ( ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ ) ↔ ( 𝐺 ∉ V ∨ ¬ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) ) )
8 orass ⊢ ( ( ( ¬ 𝐺 ∈ V ∨ ¬ 𝑁 ∈ ℕ0 ) ∨ ¬ 𝑁 ≠ 0 ) ↔ ( ¬ 𝐺 ∈ V ∨ ( ¬ 𝑁 ∈ ℕ0 ∨ ¬ 𝑁 ≠ 0 ) ) )
9 3 7 8 3bitr4i ⊢ ( ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ ) ↔ ( ( ¬ 𝐺 ∈ V ∨ ¬ 𝑁 ∈ ℕ0 ) ∨ ¬ 𝑁 ≠ 0 ) )
10 ianor ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ↔ ( ¬ 𝑁 ∈ ℕ0 ∨ ¬ 𝐺 ∈ V ) )
11 orcom ⊢ ( ( ¬ 𝑁 ∈ ℕ0 ∨ ¬ 𝐺 ∈ V ) ↔ ( ¬ 𝐺 ∈ V ∨ ¬ 𝑁 ∈ ℕ0 ) )
12 10 11 bitri ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ↔ ( ¬ 𝐺 ∈ V ∨ ¬ 𝑁 ∈ ℕ0 ) )
13 df-clwwlkn ⊢ ClWWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } )
14 13 mpondm0 ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 ClWWalksN 𝐺 ) = ∅ )
15 12 14 sylbir ⊢ ( ( ¬ 𝐺 ∈ V ∨ ¬ 𝑁 ∈ ℕ0 ) → ( 𝑁 ClWWalksN 𝐺 ) = ∅ )
16 nne ⊢ ( ¬ 𝑁 ≠ 0 ↔ 𝑁 = 0 )
17 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 ClWWalksN 𝐺 ) = ( 0 ClWWalksN 𝐺 ) )
18 clwwlkn0 ⊢ ( 0 ClWWalksN 𝐺 ) = ∅
19 17 18 eqtrdi ⊢ ( 𝑁 = 0 → ( 𝑁 ClWWalksN 𝐺 ) = ∅ )
20 16 19 sylbi ⊢ ( ¬ 𝑁 ≠ 0 → ( 𝑁 ClWWalksN 𝐺 ) = ∅ )
21 15 20 jaoi ⊢ ( ( ( ¬ 𝐺 ∈ V ∨ ¬ 𝑁 ∈ ℕ0 ) ∨ ¬ 𝑁 ≠ 0 ) → ( 𝑁 ClWWalksN 𝐺 ) = ∅ )
22 9 21 sylbi ⊢ ( ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ ) → ( 𝑁 ClWWalksN 𝐺 ) = ∅ )