dlwwlknondlwlknonf1o

Description: F is a bijection between the two representations of double loops of a fixed positive length on a fixed vertex. (Contributed by AV, 30-May-2022) (Revised by AV, 1-Nov-2022)

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

Proof

Step	Hyp	Ref	Expression
1		dlwwlknondlwlknonbij.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dlwwlknondlwlknonbij.w	⊢ 𝑊 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
3		dlwwlknondlwlknonbij.d	⊢ 𝐷 = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 }
4		dlwwlknondlwlknonf1o.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑊 ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
5		df-3an	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ∧ ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
6	5	rabbii	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ∧ ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
7	2 6	eqtri	⊢ 𝑊 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ∧ ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
8		eqid	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
9		eqid	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) = ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
10		eluz2nn	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 2 ) → 𝑁 ∈ ℕ )
11	1 8 9	clwwlknonclwlknonf1o	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
12	10 11	syl3an3	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
13		fveq1	⊢ ( 𝑦 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) → ( 𝑦 ‘ ( 𝑁 − 2 ) ) = ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ ( 𝑁 − 2 ) ) )
14	13	3ad2ant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ∧ 𝑦 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( 𝑦 ‘ ( 𝑁 − 2 ) ) = ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ ( 𝑁 − 2 ) ) )
15		2fveq3	⊢ ( 𝑤 = 𝑐 → ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) )
16	15	eqeq1d	⊢ ( 𝑤 = 𝑐 → ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ↔ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) )
17		fveq2	⊢ ( 𝑤 = 𝑐 → ( 2^nd ‘ 𝑤 ) = ( 2^nd ‘ 𝑐 ) )
18	17	fveq1d	⊢ ( 𝑤 = 𝑐 → ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) )
19	18	eqeq1d	⊢ ( 𝑤 = 𝑐 → ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ↔ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 ) )
20	16 19	anbi12d	⊢ ( 𝑤 = 𝑐 → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 ) ) )
21	20	elrab	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ↔ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 ) ) )
22		simplrl	⊢ ( ( ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 ) ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ) → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 )
23		simpll	⊢ ( ( ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 ) ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ) → 𝑐 ∈ ( ClWalks ‘ 𝐺 ) )
24		simpr3	⊢ ( ( ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 ) ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ) → 𝑁 ∈ ( ℤ_≥ ‘ 2 ) )
25	22 23 24	3jca	⊢ ( ( ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 ) ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) )
26	25	ex	⊢ ( ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = 𝑋 ) ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ) )
27	21 26	sylbi	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } → ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ) )
28	27	impcom	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) )
29		dlwwlknondlwlknonf1olem1	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ ( 𝑁 − 2 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) )
30	28 29	syl	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) → ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ ( 𝑁 − 2 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) )
31	30	3adant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ∧ 𝑦 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ ( 𝑁 − 2 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) )
32	14 31	eqtrd	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ∧ 𝑦 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( 𝑦 ‘ ( 𝑁 − 2 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) )
33	32	eqeq1d	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ∧ 𝑦 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( ( 𝑦 ‘ ( 𝑁 − 2 ) ) = 𝑋 ↔ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
34		nfv	⊢ Ⅎ 𝑤 ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) = 𝑋
35	17	fveq1d	⊢ ( 𝑤 = 𝑐 → ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) )
36	35	eqeq1d	⊢ ( 𝑤 = 𝑐 → ( ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ↔ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
37	34 36	sbiev	⊢ ( [ 𝑐 / 𝑤 ] ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ↔ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 )
38	33 37	bitr4di	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ∧ 𝑦 = ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( ( 𝑦 ‘ ( 𝑁 − 2 ) ) = 𝑋 ↔ [ 𝑐 / 𝑤 ] ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
39	7 8 4 9 12 38	f1ossf1o	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → 𝐹 : 𝑊 –1-1-onto→ { 𝑦 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑦 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
40		fveq1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ‘ ( 𝑁 − 2 ) ) = ( 𝑦 ‘ ( 𝑁 − 2 ) ) )
41	40	eqeq1d	⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ↔ ( 𝑦 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
42	41	cbvrabv	⊢ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } = { 𝑦 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑦 ‘ ( 𝑁 − 2 ) ) = 𝑋 }
43	3 42	eqtri	⊢ 𝐷 = { 𝑦 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑦 ‘ ( 𝑁 − 2 ) ) = 𝑋 }
44		f1oeq3	⊢ ( 𝐷 = { 𝑦 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑦 ‘ ( 𝑁 − 2 ) ) = 𝑋 } → ( 𝐹 : 𝑊 –1-1-onto→ 𝐷 ↔ 𝐹 : 𝑊 –1-1-onto→ { 𝑦 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑦 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) )
45	43 44	ax-mp	⊢ ( 𝐹 : 𝑊 –1-1-onto→ 𝐷 ↔ 𝐹 : 𝑊 –1-1-onto→ { 𝑦 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑦 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
46	39 45	sylibr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → 𝐹 : 𝑊 –1-1-onto→ 𝐷 )

Metamath Proof Explorer

Theorem dlwwlknondlwlknonf1o

Proof