clwwlknon

Description: The set of closed walks on vertex X of length N in a graph G as words over the set of vertices. (Contributed by Alexander van der Vekens, 14-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 24-Mar-2022)

		Ref	Expression
	Assertion	clwwlknon	$⊢ X ClWWalksNOn (G) N = \{w \in (N ClWWalksN G) \| w (0) = X\}$

Proof

Step	Hyp	Ref	Expression
1		eqeq2	$⊢ v = X \to (w (0) = v \leftrightarrow w (0) = X)$
2	1	rabbidv	$⊢ v = X \to \{w \in (n ClWWalksN G) \| w (0) = v\} = \{w \in (n ClWWalksN G) \| w (0) = X\}$
3		oveq1	$⊢ n = N \to n ClWWalksN G = N ClWWalksN G$
4	3	rabeqdv	$⊢ n = N \to \{w \in (n ClWWalksN G) \| w (0) = X\} = \{w \in (N ClWWalksN G) \| w (0) = X\}$
5		clwwlknonmpo	$⊢ ClWWalksNOn (G) = (v \in Vtx (G), n \in ℕ_{0} ⟼ \{w \in (n ClWWalksN G) \| w (0) = v\})$
6		ovex	$⊢ N ClWWalksN G \in V$
7	6	rabex	$⊢ \{w \in (N ClWWalksN G) \| w (0) = X\} \in V$
8	2 4 5 7	ovmpo	$⊢ (X \in Vtx (G) \land N \in ℕ_{0}) \to X ClWWalksNOn (G) N = \{w \in (N ClWWalksN G) \| w (0) = X\}$
9	5	mpondm0	$⊢ \neg (X \in Vtx (G) \land N \in ℕ_{0}) \to X ClWWalksNOn (G) N = \emptyset$
10		isclwwlkn	$⊢ w \in (N ClWWalksN G) \leftrightarrow (w \in ClWWalks (G) \land \|w\| = N)$
11		eqid	$⊢ Vtx (G) = Vtx (G)$
12	11	clwwlkbp	$⊢ w \in ClWWalks (G) \to (G \in V \land w \in Word Vtx (G) \land w \neq \emptyset)$
13		fstwrdne	$⊢ (w \in Word Vtx (G) \land w \neq \emptyset) \to w (0) \in Vtx (G)$
14	13	3adant1	$⊢ (G \in V \land w \in Word Vtx (G) \land w \neq \emptyset) \to w (0) \in Vtx (G)$
15	12 14	syl	$⊢ w \in ClWWalks (G) \to w (0) \in Vtx (G)$
16	15	adantr	$⊢ (w \in ClWWalks (G) \land \|w\| = N) \to w (0) \in Vtx (G)$
17	10 16	sylbi	$⊢ w \in (N ClWWalksN G) \to w (0) \in Vtx (G)$
18	17	adantr	$⊢ (w \in (N ClWWalksN G) \land w (0) = X) \to w (0) \in Vtx (G)$
19		eleq1	$⊢ w (0) = X \to (w (0) \in Vtx (G) \leftrightarrow X \in Vtx (G))$
20	19	adantl	$⊢ (w \in (N ClWWalksN G) \land w (0) = X) \to (w (0) \in Vtx (G) \leftrightarrow X \in Vtx (G))$
21	18 20	mpbid	$⊢ (w \in (N ClWWalksN G) \land w (0) = X) \to X \in Vtx (G)$
22		clwwlknnn	$⊢ w \in (N ClWWalksN G) \to N \in ℕ$
23	22	nnnn0d	$⊢ w \in (N ClWWalksN G) \to N \in ℕ_{0}$
24	23	adantr	$⊢ (w \in (N ClWWalksN G) \land w (0) = X) \to N \in ℕ_{0}$
25	21 24	jca	$⊢ (w \in (N ClWWalksN G) \land w (0) = X) \to (X \in Vtx (G) \land N \in ℕ_{0})$
26	25	ex	$⊢ w \in (N ClWWalksN G) \to (w (0) = X \to (X \in Vtx (G) \land N \in ℕ_{0}))$
27	26	con3rr3	$⊢ \neg (X \in Vtx (G) \land N \in ℕ_{0}) \to (w \in (N ClWWalksN G) \to \neg w (0) = X)$
28	27	ralrimiv	$⊢ \neg (X \in Vtx (G) \land N \in ℕ_{0}) \to \forall w \in (N ClWWalksN G) \neg w (0) = X$
29		rabeq0	$⊢ \{w \in (N ClWWalksN G) \| w (0) = X\} = \emptyset \leftrightarrow \forall w \in (N ClWWalksN G) \neg w (0) = X$
30	28 29	sylibr	$⊢ \neg (X \in Vtx (G) \land N \in ℕ_{0}) \to \{w \in (N ClWWalksN G) \| w (0) = X\} = \emptyset$
31	9 30	eqtr4d	$⊢ \neg (X \in Vtx (G) \land N \in ℕ_{0}) \to X ClWWalksNOn (G) N = \{w \in (N ClWWalksN G) \| w (0) = X\}$
32	8 31	pm2.61i	$⊢ X ClWWalksNOn (G) N = \{w \in (N ClWWalksN G) \| w (0) = X\}$

Metamath Proof Explorer

Theorem clwwlknon

Proof