clwwlknonclwlknonf1o

Description: F is a bijection between the two representations of closed walks of a fixed positive length on a fixed vertex. (Contributed by AV, 26-May-2022) (Proof shortened by AV, 7-Aug-2022) (Revised by AV, 1-Nov-2022)

	Ref	Expression
Hypotheses	clwwlknonclwlknonf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	clwwlknonclwlknonf1o.w	⊢ 𝑊 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
	clwwlknonclwlknonf1o.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑊 ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
Assertion	clwwlknonclwlknonf1o	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝐹 : 𝑊 –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlknonclwlknonf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clwwlknonclwlknonf1o.w	⊢ 𝑊 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
3		clwwlknonclwlknonf1o.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑊 ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
4		eqid	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 }
5		eqid	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) = ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
6		eqid	⊢ ( 1^st ‘ 𝑐 ) = ( 1^st ‘ 𝑐 )
7		eqid	⊢ ( 2^nd ‘ 𝑐 ) = ( 2^nd ‘ 𝑐 )
8	6 7 4 5	clwlknf1oclwwlkn	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) )
9	8	3adant2	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) )
10		fveq1	⊢ ( 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) → ( 𝑠 ‘ 0 ) = ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ 0 ) )
11	10	3ad2ant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ∧ 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( 𝑠 ‘ 0 ) = ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ 0 ) )
12		2fveq3	⊢ ( 𝑤 = 𝑐 → ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) )
13	12	eqeq1d	⊢ ( 𝑤 = 𝑐 → ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ↔ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) )
14	13	elrab	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ↔ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) )
15		clwlkwlk	⊢ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) → 𝑐 ∈ ( Walks ‘ 𝐺 ) )
16		wlkcpr	⊢ ( 𝑐 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) )
17		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
18	17	wlkpwrd	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) )
19	18	3ad2ant1	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) )
20		elnnuz	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ_≥ ‘ 1 ) )
21		eluzfz2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 1 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
22	20 21	sylbi	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 1 ... 𝑁 ) )
23		fzelp1	⊢ ( 𝑁 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
24	22 23	syl	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
25	24	3ad2ant3	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
26	25	3ad2ant3	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
27		id	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 )
28		oveq1	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) = ( 𝑁 + 1 ) )
29	28	oveq2d	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( 1 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
30	27 29	eleq12d	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
31	30	3ad2ant2	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
32	26 31	mpbird	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) )
33		wlklenvp1	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) )
34	33	oveq2d	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) = ( 1 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) )
35	34	eleq2d	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) ) )
36	35	3ad2ant1	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) ) )
37	32 36	mpbird	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) )
38	19 37	jca	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) )
39	38	3exp	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) ) ) )
40	16 39	sylbi	⊢ ( 𝑐 ∈ ( Walks ‘ 𝐺 ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) ) ) )
41	15 40	syl	⊢ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) ) ) )
42	41	imp	⊢ ( ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) ) )
43	14 42	sylbi	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } → ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) ) )
44	43	impcom	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ) → ( ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) )
45		pfxfv0	⊢ ( ( ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 1 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) → ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) )
46	44 45	syl	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ) → ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) )
47	46	3adant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ∧ 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) )
48	11 47	eqtrd	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ∧ 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( 𝑠 ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) )
49	48	eqeq1d	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ∧ 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( ( 𝑠 ‘ 0 ) = 𝑋 ↔ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 ) )
50		nfv	⊢ Ⅎ 𝑤 ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋
51		fveq2	⊢ ( 𝑤 = 𝑐 → ( 2^nd ‘ 𝑤 ) = ( 2^nd ‘ 𝑐 ) )
52	51	fveq1d	⊢ ( 𝑤 = 𝑐 → ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) )
53	52	eqeq1d	⊢ ( 𝑤 = 𝑐 → ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ↔ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 ) )
54	50 53	sbiev	⊢ ( [ 𝑐 / 𝑤 ] ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ↔ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 )
55	49 54	bitr4di	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } ∧ 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( ( 𝑠 ‘ 0 ) = 𝑋 ↔ [ 𝑐 / 𝑤 ] ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) )
56	2 4 3 5 9 55	f1ossf1o	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝐹 : 𝑊 –1-1-onto→ { 𝑠 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑠 ‘ 0 ) = 𝑋 } )
57		clwwlknon	⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑠 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑠 ‘ 0 ) = 𝑋 }
58		f1oeq3	⊢ ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑠 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑠 ‘ 0 ) = 𝑋 } → ( 𝐹 : 𝑊 –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ 𝐹 : 𝑊 –1-1-onto→ { 𝑠 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑠 ‘ 0 ) = 𝑋 } ) )
59	57 58	ax-mp	⊢ ( 𝐹 : 𝑊 –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ 𝐹 : 𝑊 –1-1-onto→ { 𝑠 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑠 ‘ 0 ) = 𝑋 } )
60	56 59	sylibr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝐹 : 𝑊 –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )

Metamath Proof Explorer

Theorem clwwlknonclwlknonf1o

Proof