Metamath Proof Explorer

Theorem wspthsn

Description: The set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 11-May-2021)

		Ref	Expression
	Assertion	wspthsn	$⊢ N WSPathsN G = \{w \in (N WWalksN G) \| \exists f f SPaths (G) w\}$

Proof

Step	Hyp	Ref	Expression
1		oveq12	$⊢ (n = N \land g = G) \to n WWalksN g = N WWalksN G$
2		fveq2	$⊢ g = G \to SPaths (g) = SPaths (G)$
3	2	breqd	$⊢ g = G \to (f SPaths (g) w \leftrightarrow f SPaths (G) w)$
4	3	exbidv	$⊢ g = G \to (\exists f f SPaths (g) w \leftrightarrow \exists f f SPaths (G) w)$
5	4	adantl	$⊢ (n = N \land g = G) \to (\exists f f SPaths (g) w \leftrightarrow \exists f f SPaths (G) w)$
6	1 5	rabeqbidv	$⊢ (n = N \land g = G) \to \{w \in (n WWalksN g) \| \exists f f SPaths (g) w\} = \{w \in (N WWalksN G) \| \exists f f SPaths (G) w\}$
7		df-wspthsn	$⊢ WSPathsN = (n \in ℕ_{0}, g \in V ⟼ \{w \in (n WWalksN g) \| \exists f f SPaths (g) w\})$
8		ovex	$⊢ N WWalksN G \in V$
9	8	rabex	$⊢ \{w \in (N WWalksN G) \| \exists f f SPaths (G) w\} \in V$
10	6 7 9	ovmpoa	$⊢ (N \in ℕ_{0} \land G \in V) \to N WSPathsN G = \{w \in (N WWalksN G) \| \exists f f SPaths (G) w\}$
11	7	mpondm0	$⊢ \neg (N \in ℕ_{0} \land G \in V) \to N WSPathsN G = \emptyset$
12		df-wwlksn	$⊢ WWalksN = (n \in ℕ_{0}, g \in V ⟼ \{w \in WWalks (g) \| \|w\| = n + 1\})$
13	12	mpondm0	$⊢ \neg (N \in ℕ_{0} \land G \in V) \to N WWalksN G = \emptyset$
14	13	rabeqdv	$⊢ \neg (N \in ℕ_{0} \land G \in V) \to \{w \in (N WWalksN G) \| \exists f f SPaths (G) w\} = \{w \in \emptyset \| \exists f f SPaths (G) w\}$
15		rab0	$⊢ \{w \in \emptyset \| \exists f f SPaths (G) w\} = \emptyset$
16	14 15	eqtrdi	$⊢ \neg (N \in ℕ_{0} \land G \in V) \to \{w \in (N WWalksN G) \| \exists f f SPaths (G) w\} = \emptyset$
17	11 16	eqtr4d	$⊢ \neg (N \in ℕ_{0} \land G \in V) \to N WSPathsN G = \{w \in (N WWalksN G) \| \exists f f SPaths (G) w\}$
18	10 17	pm2.61i	$⊢ N WSPathsN G = \{w \in (N WWalksN G) \| \exists f f SPaths (G) w\}$