clwwlkvbij

Description: There is a bijection between the set of closed walks of a fixed length N on a fixed vertex X represented by walks (as word) and the set of closed walks (as words) of the fixed length N on the fixed vertex X . The difference between these two representations is that in the first case the fixed vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 7-Jul-2022) (Proof shortened by AV, 2-Nov-2022)

		Ref	Expression
	Assertion	clwwlkvbij	$⊢ (X \in V \land N \in ℕ) \to \exists f f : \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ N WWalksN G \in V$
2	1	mptrabex	$⊢ (w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) \in V$
3	2	resex	$⊢ {(w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) ↾}_{\{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}} \in V$
4		eqid	$⊢ (w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) = (w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N)$
5		eqid	$⊢ \{x \in (N WWalksN G) \| lastS (x) = x (0)\} = \{x \in (N WWalksN G) \| lastS (x) = x (0)\}$
6	5 4	clwwlkf1o	$⊢ N \in ℕ \to (w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) : \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \underset{1-1 onto}{⟶} N ClWWalksN G$
7		fveq1	$⊢ y = w prefix N \to y (0) = (w prefix N) (0)$
8	7	eqeq1d	$⊢ y = w prefix N \to (y (0) = X \leftrightarrow (w prefix N) (0) = X)$
9	8	3ad2ant3	$⊢ (N \in ℕ \land w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \land y = w prefix N) \to (y (0) = X \leftrightarrow (w prefix N) (0) = X)$
10		fveq2	$⊢ x = w \to lastS (x) = lastS (w)$
11		fveq1	$⊢ x = w \to x (0) = w (0)$
12	10 11	eqeq12d	$⊢ x = w \to (lastS (x) = x (0) \leftrightarrow lastS (w) = w (0))$
13	12	elrab	$⊢ w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \leftrightarrow (w \in (N WWalksN G) \land lastS (w) = w (0))$
14		eqid	$⊢ Vtx (G) = Vtx (G)$
15		eqid	$⊢ Edg (G) = Edg (G)$
16	14 15	wwlknp	$⊢ w \in (N WWalksN G) \to (w \in Word Vtx (G) \land \|w\| = N + 1 \land \forall i \in (0 ..^N) \{w (i), w (i + 1)\} \in Edg (G))$
17		simpll	$⊢ ((w \in Word Vtx (G) \land \|w\| = N + 1) \land N \in ℕ) \to w \in Word Vtx (G)$
18		nnz	$⊢ N \in ℕ \to N \in ℤ$
19		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
20		peano2uz	$⊢ N \in ℤ_{\geq N} \to N + 1 \in ℤ_{\geq N}$
21	18 19 20	3syl	$⊢ N \in ℕ \to N + 1 \in ℤ_{\geq N}$
22		elfz1end	$⊢ N \in ℕ \leftrightarrow N \in (1 \dots N)$
23	22	biimpi	$⊢ N \in ℕ \to N \in (1 \dots N)$
24		fzss2	$⊢ N + 1 \in ℤ_{\geq N} \to (1 \dots N) \subseteq (1 \dots N + 1)$
25	24	sselda	$⊢ (N + 1 \in ℤ_{\geq N} \land N \in (1 \dots N)) \to N \in (1 \dots N + 1)$
26	21 23 25	syl2anc	$⊢ N \in ℕ \to N \in (1 \dots N + 1)$
27	26	adantl	$⊢ ((w \in Word Vtx (G) \land \|w\| = N + 1) \land N \in ℕ) \to N \in (1 \dots N + 1)$
28		oveq2	$⊢ \|w\| = N + 1 \to (1 \dots \|w\|) = (1 \dots N + 1)$
29	28	eleq2d	$⊢ \|w\| = N + 1 \to (N \in (1 \dots \|w\|) \leftrightarrow N \in (1 \dots N + 1))$
30	29	adantl	$⊢ (w \in Word Vtx (G) \land \|w\| = N + 1) \to (N \in (1 \dots \|w\|) \leftrightarrow N \in (1 \dots N + 1))$
31	30	adantr	$⊢ ((w \in Word Vtx (G) \land \|w\| = N + 1) \land N \in ℕ) \to (N \in (1 \dots \|w\|) \leftrightarrow N \in (1 \dots N + 1))$
32	27 31	mpbird	$⊢ ((w \in Word Vtx (G) \land \|w\| = N + 1) \land N \in ℕ) \to N \in (1 \dots \|w\|)$
33	17 32	jca	$⊢ ((w \in Word Vtx (G) \land \|w\| = N + 1) \land N \in ℕ) \to (w \in Word Vtx (G) \land N \in (1 \dots \|w\|))$
34	33	ex	$⊢ (w \in Word Vtx (G) \land \|w\| = N + 1) \to (N \in ℕ \to (w \in Word Vtx (G) \land N \in (1 \dots \|w\|)))$
35	34	3adant3	$⊢ (w \in Word Vtx (G) \land \|w\| = N + 1 \land \forall i \in (0 ..^N) \{w (i), w (i + 1)\} \in Edg (G)) \to (N \in ℕ \to (w \in Word Vtx (G) \land N \in (1 \dots \|w\|)))$
36	16 35	syl	$⊢ w \in (N WWalksN G) \to (N \in ℕ \to (w \in Word Vtx (G) \land N \in (1 \dots \|w\|)))$
37	36	adantr	$⊢ (w \in (N WWalksN G) \land lastS (w) = w (0)) \to (N \in ℕ \to (w \in Word Vtx (G) \land N \in (1 \dots \|w\|)))$
38	13 37	sylbi	$⊢ w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \to (N \in ℕ \to (w \in Word Vtx (G) \land N \in (1 \dots \|w\|)))$
39	38	impcom	$⊢ (N \in ℕ \land w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\}) \to (w \in Word Vtx (G) \land N \in (1 \dots \|w\|))$
40		pfxfv0	$⊢ (w \in Word Vtx (G) \land N \in (1 \dots \|w\|)) \to (w prefix N) (0) = w (0)$
41	39 40	syl	$⊢ (N \in ℕ \land w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\}) \to (w prefix N) (0) = w (0)$
42	41	eqeq1d	$⊢ (N \in ℕ \land w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\}) \to ((w prefix N) (0) = X \leftrightarrow w (0) = X)$
43	42	3adant3	$⊢ (N \in ℕ \land w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \land y = w prefix N) \to ((w prefix N) (0) = X \leftrightarrow w (0) = X)$
44	9 43	bitrd	$⊢ (N \in ℕ \land w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \land y = w prefix N) \to (y (0) = X \leftrightarrow w (0) = X)$
45	4 6 44	f1oresrab	$⊢ N \in ℕ \to ({(w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) ↾}_{\{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}}) : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} \{y \in (N ClWWalksN G) \| y (0) = X\}$
46	45	adantl	$⊢ (X \in V \land N \in ℕ) \to ({(w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) ↾}_{\{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}}) : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} \{y \in (N ClWWalksN G) \| y (0) = X\}$
47		clwwlknon	$⊢ X ClWWalksNOn (G) N = \{y \in (N ClWWalksN G) \| y (0) = X\}$
48	47	a1i	$⊢ (X \in V \land N \in ℕ) \to X ClWWalksNOn (G) N = \{y \in (N ClWWalksN G) \| y (0) = X\}$
49	48	f1oeq3d	$⊢ (X \in V \land N \in ℕ) \to (({(w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) ↾}_{\{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}}) : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N \leftrightarrow ({(w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) ↾}_{\{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}}) : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} \{y \in (N ClWWalksN G) \| y (0) = X\})$
50	46 49	mpbird	$⊢ (X \in V \land N \in ℕ) \to ({(w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) ↾}_{\{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}}) : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N$
51		f1oeq1	$⊢ f = {(w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) ↾}_{\{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}} \to (f : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N \leftrightarrow ({(w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) ↾}_{\{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}}) : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N)$
52	51	spcegv	$⊢ {(w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) ↾}_{\{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}} \in V \to (({(w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} ⟼ w prefix N) ↾}_{\{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}}) : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N \to \exists f f : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N)$
53	3 50 52	mpsyl	$⊢ (X \in V \land N \in ℕ) \to \exists f f : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N$
54		df-rab	$⊢ \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} = \{w \| (w \in (N WWalksN G) \land (lastS (w) = w (0) \land w (0) = X))\}$
55		anass	$⊢ ((w \in (N WWalksN G) \land lastS (w) = w (0)) \land w (0) = X) \leftrightarrow (w \in (N WWalksN G) \land (lastS (w) = w (0) \land w (0) = X))$
56	55	bicomi	$⊢ (w \in (N WWalksN G) \land (lastS (w) = w (0) \land w (0) = X)) \leftrightarrow ((w \in (N WWalksN G) \land lastS (w) = w (0)) \land w (0) = X)$
57	56	abbii	$⊢ \{w \| (w \in (N WWalksN G) \land (lastS (w) = w (0) \land w (0) = X))\} = \{w \| ((w \in (N WWalksN G) \land lastS (w) = w (0)) \land w (0) = X)\}$
58	13	bicomi	$⊢ (w \in (N WWalksN G) \land lastS (w) = w (0)) \leftrightarrow w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\}$
59	58	anbi1i	$⊢ ((w \in (N WWalksN G) \land lastS (w) = w (0)) \land w (0) = X) \leftrightarrow (w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \land w (0) = X)$
60	59	abbii	$⊢ \{w \| ((w \in (N WWalksN G) \land lastS (w) = w (0)) \land w (0) = X)\} = \{w \| (w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \land w (0) = X)\}$
61		df-rab	$⊢ \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} = \{w \| (w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \land w (0) = X)\}$
62	60 61	eqtr4i	$⊢ \{w \| ((w \in (N WWalksN G) \land lastS (w) = w (0)) \land w (0) = X)\} = \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}$
63	54 57 62	3eqtri	$⊢ \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} = \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\}$
64		f1oeq2	$⊢ \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} = \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \to (f : \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N \leftrightarrow f : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N)$
65	63 64	mp1i	$⊢ (X \in V \land N \in ℕ) \to (f : \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N \leftrightarrow f : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N)$
66	65	exbidv	$⊢ (X \in V \land N \in ℕ) \to (\exists f f : \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N \leftrightarrow \exists f f : \{w \in \{x \in (N WWalksN G) \| lastS (x) = x (0)\} \| w (0) = X\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N)$
67	53 66	mpbird	$⊢ (X \in V \land N \in ℕ) \to \exists f f : \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N$

Metamath Proof Explorer

Theorem clwwlkvbij

Proof