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 \notin V \lor N \notin ℕ_{0}) \to N WWalksN G = \emptyset$

Step	Hyp	Ref	Expression
1		neq0	$⊢ \neg N WWalksN G = \emptyset \leftrightarrow \exists w w \in (N WWalksN G)$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3	2	wwlknbp	$⊢ w \in (N WWalksN G) \to (G \in V \land N \in ℕ_{0} \land w \in Word Vtx (G))$
4		nnel	$⊢ \neg G \notin V \leftrightarrow G \in V$
5		nnel	$⊢ \neg N \notin ℕ_{0} \leftrightarrow N \in ℕ_{0}$
6	4 5	anbi12i	$⊢ (\neg G \notin V \land \neg N \notin ℕ_{0}) \leftrightarrow (G \in V \land N \in ℕ_{0})$
7	6	biimpri	$⊢ (G \in V \land N \in ℕ_{0}) \to (\neg G \notin V \land \neg N \notin ℕ_{0})$
8	7	3adant3	$⊢ (G \in V \land N \in ℕ_{0} \land w \in Word Vtx (G)) \to (\neg G \notin V \land \neg N \notin ℕ_{0})$
9		ioran	$⊢ \neg (G \notin V \lor N \notin ℕ_{0}) \leftrightarrow (\neg G \notin V \land \neg N \notin ℕ_{0})$
10	8 9	sylibr	$⊢ (G \in V \land N \in ℕ_{0} \land w \in Word Vtx (G)) \to \neg (G \notin V \lor N \notin ℕ_{0})$
11	3 10	syl	$⊢ w \in (N WWalksN G) \to \neg (G \notin V \lor N \notin ℕ_{0})$
12	11	exlimiv	$⊢ \exists w w \in (N WWalksN G) \to \neg (G \notin V \lor N \notin ℕ_{0})$
13	1 12	sylbi	$⊢ \neg N WWalksN G = \emptyset \to \neg (G \notin V \lor N \notin ℕ_{0})$
14	13	con4i	$⊢ (G \notin V \lor N \notin ℕ_{0}) \to N WWalksN G = \emptyset$

Metamath Proof Explorer