clwwlknon0

Description: Sufficient conditions for ClWWalksNOn to be empty. (Contributed by AV, 25-Mar-2022)

		Ref	Expression
	Assertion	clwwlknon0	$⊢ \neg (X \in Vtx (G) \land N \in ℕ) \to X ClWWalksNOn (G) N = \emptyset$

Step	Hyp	Ref	Expression
1		oveq2	$⊢ N = 0 \to X ClWWalksNOn (G) N = X ClWWalksNOn (G) 0$
2		clwwlk0on0	$⊢ X ClWWalksNOn (G) 0 = \emptyset$
3	1 2	eqtrdi	$⊢ N = 0 \to X ClWWalksNOn (G) N = \emptyset$
4	3	a1d	$⊢ N = 0 \to (\neg (X \in Vtx (G) \land N \in ℕ) \to X ClWWalksNOn (G) N = \emptyset)$
5		simprl	$⊢ (N \neq 0 \land (X \in Vtx (G) \land N \in ℕ_{0})) \to X \in Vtx (G)$
6		elnnne0	$⊢ N \in ℕ \leftrightarrow (N \in ℕ_{0} \land N \neq 0)$
7	6	simplbi2	$⊢ N \in ℕ_{0} \to (N \neq 0 \to N \in ℕ)$
8	7	adantl	$⊢ (X \in Vtx (G) \land N \in ℕ_{0}) \to (N \neq 0 \to N \in ℕ)$
9	8	impcom	$⊢ (N \neq 0 \land (X \in Vtx (G) \land N \in ℕ_{0})) \to N \in ℕ$
10	5 9	jca	$⊢ (N \neq 0 \land (X \in Vtx (G) \land N \in ℕ_{0})) \to (X \in Vtx (G) \land N \in ℕ)$
11	10	stoic1a	$⊢ (N \neq 0 \land \neg (X \in Vtx (G) \land N \in ℕ)) \to \neg (X \in Vtx (G) \land N \in ℕ_{0})$
12		clwwlknonmpo	$⊢ ClWWalksNOn (G) = (v \in Vtx (G), n \in ℕ_{0} ⟼ \{w \in (n ClWWalksN G) \| w (0) = v\})$
13	12	mpondm0	$⊢ \neg (X \in Vtx (G) \land N \in ℕ_{0}) \to X ClWWalksNOn (G) N = \emptyset$
14	11 13	syl	$⊢ (N \neq 0 \land \neg (X \in Vtx (G) \land N \in ℕ)) \to X ClWWalksNOn (G) N = \emptyset$
15	14	ex	$⊢ N \neq 0 \to (\neg (X \in Vtx (G) \land N \in ℕ) \to X ClWWalksNOn (G) N = \emptyset)$
16	4 15	pm2.61ine	$⊢ \neg (X \in Vtx (G) \land N \in ℕ) \to X ClWWalksNOn (G) N = \emptyset$

Metamath Proof Explorer