Theorem 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	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( 𝑁 WWalksN 𝐺 ) ∈ V
2	1	mptrabex	⊢ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ∈ V
3	2	resex	⊢ ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) ∈ V
4		eqid	⊢ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) = ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) )
5		eqid	⊢ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } = { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) }
6	5 4	clwwlkf1o	⊢ ( 𝑁 ∈ ℕ → ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) : { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) )
7		fveq1	⊢ ( 𝑦 = ( 𝑤 prefix 𝑁 ) → ( 𝑦 ‘ 0 ) = ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) )
8	7	eqeq1d	⊢ ( 𝑦 = ( 𝑤 prefix 𝑁 ) → ( ( 𝑦 ‘ 0 ) = 𝑋 ↔ ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = 𝑋 ) )
9	8	3ad2ant3	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ 𝑦 = ( 𝑤 prefix 𝑁 ) ) → ( ( 𝑦 ‘ 0 ) = 𝑋 ↔ ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = 𝑋 ) )
10		fveq2	⊢ ( 𝑥 = 𝑤 → ( lastS ‘ 𝑥 ) = ( lastS ‘ 𝑤 ) )
11		fveq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 ‘ 0 ) = ( 𝑤 ‘ 0 ) )
12	10 11	eqeq12d	⊢ ( 𝑥 = 𝑤 → ( ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ↔ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) )
13	12	elrab	⊢ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↔ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) )
14		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
15		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
16	14 15	wwlknp	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
17		simpll	⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
18		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
19		uzid	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
20		peano2uz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
21	18 19 20	3syl	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
22		elfz1end	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( 1 ... 𝑁 ) )
23	22	biimpi	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 1 ... 𝑁 ) )
24		fzss2	⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 1 ... 𝑁 ) ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
25	24	sselda	⊢ ( ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
26	21 23 25	syl2anc	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
27	26	adantl	⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
28		oveq2	⊢ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ( 1 ... ( ♯ ‘ 𝑤 ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
29	28	eleq2d	⊢ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
30	29	adantl	⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
31	30	adantr	⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
32	27 31	mpbird	⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) )
33	17 32	jca	⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) )
34	33	ex	⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ℕ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ) )
35	34	3adant3	⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑁 ∈ ℕ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ) )
36	16 35	syl	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ) )
37	36	adantr	⊢ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ) )
38	13 37	sylbi	⊢ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } → ( 𝑁 ∈ ℕ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ) )
39	38	impcom	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) )
40		pfxfv0	⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) → ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = ( 𝑤 ‘ 0 ) )
41	39 40	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ) → ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = ( 𝑤 ‘ 0 ) )
42	41	eqeq1d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ) → ( ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = 𝑋 ↔ ( 𝑤 ‘ 0 ) = 𝑋 ) )
43	42	3adant3	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ 𝑦 = ( 𝑤 prefix 𝑁 ) ) → ( ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = 𝑋 ↔ ( 𝑤 ‘ 0 ) = 𝑋 ) )
44	9 43	bitrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ 𝑦 = ( 𝑤 prefix 𝑁 ) ) → ( ( 𝑦 ‘ 0 ) = 𝑋 ↔ ( 𝑤 ‘ 0 ) = 𝑋 ) )
45	4 6 44	f1oresrab	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑦 ‘ 0 ) = 𝑋 } )
46	45	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑦 ‘ 0 ) = 𝑋 } )
47		clwwlknon	⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑦 ‘ 0 ) = 𝑋 }
48	47	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑦 ‘ 0 ) = 𝑋 } )
49	48	f1oeq3d	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑦 ‘ 0 ) = 𝑋 } ) )
50	46 49	mpbird	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
51		f1oeq1	⊢ ( 𝑓 = ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) → ( 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
52	51	spcegv	⊢ ( ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) ∈ V → ( ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
53	3 50 52	mpsyl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
54		df-rab	⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } = { 𝑤 ∣ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) }
55		anass	⊢ ( ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) )
56	55	bicomi	⊢ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) ↔ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
57	56	abbii	⊢ { 𝑤 ∣ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) } = { 𝑤 ∣ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
58	13	bicomi	⊢ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ↔ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } )
59	58	anbi1i	⊢ ( ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
60	59	abbii	⊢ { 𝑤 ∣ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } = { 𝑤 ∣ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
61		df-rab	⊢ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } = { 𝑤 ∣ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
62	60 61	eqtr4i	⊢ { 𝑤 ∣ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } = { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
63	54 57 62	3eqtri	⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } = { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
64		f1oeq2	⊢ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } = { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } → ( 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
65	63 64	mp1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
66	65	exbidv	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ∃ 𝑓 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
67	53 66	mpbird	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )