wspthnp

Description: Properties of a set being a simple path of a fixed length as word. (Contributed by AV, 18-May-2021)

		Ref	Expression
	Assertion	wspthnp	$⊢ W \in (N WSPathsN G) \to ((N \in ℕ_{0} \land G \in V) \land W \in (N WWalksN G) \land \exists f f SPaths (G) W)$

Step	Hyp	Ref	Expression
1		df-wspthsn	$⊢ WSPathsN = (n \in ℕ_{0}, g \in V ⟼ \{w \in (n WWalksN g) \| \exists f f SPaths (g) w\})$
2	1	elmpocl	$⊢ W \in (N WSPathsN G) \to (N \in ℕ_{0} \land G \in V)$
3		simpl	$⊢ ((N \in ℕ_{0} \land G \in V) \land W \in (N WSPathsN G)) \to (N \in ℕ_{0} \land G \in V)$
4		iswspthn	$⊢ W \in (N WSPathsN G) \leftrightarrow (W \in (N WWalksN G) \land \exists f f SPaths (G) W)$
5	4	a1i	$⊢ (N \in ℕ_{0} \land G \in V) \to (W \in (N WSPathsN G) \leftrightarrow (W \in (N WWalksN G) \land \exists f f SPaths (G) W))$
6	5	biimpa	$⊢ ((N \in ℕ_{0} \land G \in V) \land W \in (N WSPathsN G)) \to (W \in (N WWalksN G) \land \exists f f SPaths (G) W)$
7		3anass	$⊢ ((N \in ℕ_{0} \land G \in V) \land W \in (N WWalksN G) \land \exists f f SPaths (G) W) \leftrightarrow ((N \in ℕ_{0} \land G \in V) \land (W \in (N WWalksN G) \land \exists f f SPaths (G) W))$
8	3 6 7	sylanbrc	$⊢ ((N \in ℕ_{0} \land G \in V) \land W \in (N WSPathsN G)) \to ((N \in ℕ_{0} \land G \in V) \land W \in (N WWalksN G) \land \exists f f SPaths (G) W)$
9	2 8	mpancom	$⊢ W \in (N WSPathsN G) \to ((N \in ℕ_{0} \land G \in V) \land W \in (N WWalksN G) \land \exists f f SPaths (G) W)$

Metamath Proof Explorer