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