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	$$⊢\left(G\notin \mathrm{V}\vee N\notin \mathbb{N}\right)\to N\mathrm{ClWWalksN}G=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-nel	$$⊢G\notin \mathrm{V}\leftrightarrow \neg G\in \mathrm{V}$$
2		ianor	$$⊢\neg \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)\leftrightarrow \left(\neg N\in {\mathbb{N}}_0\vee \neg N\ne 0\right)$$
3	1 2	orbi12i	$$⊢\left(G\notin \mathrm{V}\vee \neg \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)\right)\leftrightarrow \left(\neg G\in \mathrm{V}\vee \left(\neg N\in {\mathbb{N}}_0\vee \neg N\ne 0\right)\right)$$
4		df-nel	$$⊢N\notin \mathbb{N}\leftrightarrow \neg N\in \mathbb{N}$$
5		elnnne0	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$
6	4 5	xchbinx	$$⊢N\notin \mathbb{N}\leftrightarrow \neg \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$
7	6	orbi2i	$$⊢\left(G\notin \mathrm{V}\vee N\notin \mathbb{N}\right)\leftrightarrow \left(G\notin \mathrm{V}\vee \neg \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)\right)$$
8		orass	$$⊢\left(\left(\neg G\in \mathrm{V}\vee \neg N\in {\mathbb{N}}_0\right)\vee \neg N\ne 0\right)\leftrightarrow \left(\neg G\in \mathrm{V}\vee \left(\neg N\in {\mathbb{N}}_0\vee \neg N\ne 0\right)\right)$$
9	3 7 8	3bitr4i	$$⊢\left(G\notin \mathrm{V}\vee N\notin \mathbb{N}\right)\leftrightarrow \left(\left(\neg G\in \mathrm{V}\vee \neg N\in {\mathbb{N}}_0\right)\vee \neg N\ne 0\right)$$
10		ianor	$$⊢\neg \left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\leftrightarrow \left(\neg N\in {\mathbb{N}}_0\vee \neg G\in \mathrm{V}\right)$$
11		orcom	$$⊢\left(\neg N\in {\mathbb{N}}_0\vee \neg G\in \mathrm{V}\right)\leftrightarrow \left(\neg G\in \mathrm{V}\vee \neg N\in {\mathbb{N}}_0\right)$$
12	10 11	bitri	$$⊢\neg \left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\leftrightarrow \left(\neg G\in \mathrm{V}\vee \neg N\in {\mathbb{N}}_0\right)$$
13		df-clwwlkn	$$⊢\mathrm{ClWWalksN}=\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left\{w\in \mathrm{ClWWalks}\left(g\right)|\left|w\right|=n\right\}\right)$$
14	13	mpondm0	$$⊢\neg \left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\to N\mathrm{ClWWalksN}G=\varnothing$$
15	12 14	sylbir	$$⊢\left(\neg G\in \mathrm{V}\vee \neg N\in {\mathbb{N}}_0\right)\to N\mathrm{ClWWalksN}G=\varnothing$$
16		nne	$$⊢\neg N\ne 0\leftrightarrow N=0$$
17		oveq1	$$⊢N=0\to N\mathrm{ClWWalksN}G=0\mathrm{ClWWalksN}G$$
18		clwwlkn0	$$⊢0\mathrm{ClWWalksN}G=\varnothing$$
19	17 18	eqtrdi	$$⊢N=0\to N\mathrm{ClWWalksN}G=\varnothing$$
20	16 19	sylbi	$$⊢\neg N\ne 0\to N\mathrm{ClWWalksN}G=\varnothing$$
21	15 20	jaoi	$$⊢\left(\left(\neg G\in \mathrm{V}\vee \neg N\in {\mathbb{N}}_0\right)\vee \neg N\ne 0\right)\to N\mathrm{ClWWalksN}G=\varnothing$$
22	9 21	sylbi	$$⊢\left(G\notin \mathrm{V}\vee N\notin \mathbb{N}\right)\to N\mathrm{ClWWalksN}G=\varnothing$$