clwlknf1oclwwlkn

Description: There is a one-to-one onto function between the set of closed walks as words of length N and the set of closed walks of length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 3-May-2021) (Revised by AV, 1-Nov-2022)

	Ref	Expression
Hypotheses	clwlknf1oclwwlkn.a	⊢ 𝐴 = ( 1^st ‘ 𝑐 )
	clwlknf1oclwwlkn.b	⊢ 𝐵 = ( 2^nd ‘ 𝑐 )
	clwlknf1oclwwlkn.c	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 }
	clwlknf1oclwwlkn.f	⊢ 𝐹 = ( 𝑐 ∈ 𝐶 ↦ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) )
Assertion	clwlknf1oclwwlkn	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → 𝐹 : 𝐶 –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		clwlknf1oclwwlkn.a	⊢ 𝐴 = ( 1^st ‘ 𝑐 )
2		clwlknf1oclwwlkn.b	⊢ 𝐵 = ( 2^nd ‘ 𝑐 )
3		clwlknf1oclwwlkn.c	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 }
4		clwlknf1oclwwlkn.f	⊢ 𝐹 = ( 𝑐 ∈ 𝐶 ↦ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) )
5		eqid	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) = ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
6		2fveq3	⊢ ( 𝑠 = 𝑤 → ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) )
7	6	breq2d	⊢ ( 𝑠 = 𝑤 → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) ↔ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) ) )
8	7	cbvrabv	⊢ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) }
9		fveq2	⊢ ( 𝑑 = 𝑐 → ( 2^nd ‘ 𝑑 ) = ( 2^nd ‘ 𝑐 ) )
10		2fveq3	⊢ ( 𝑑 = 𝑐 → ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) = ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) )
11	10	oveq1d	⊢ ( 𝑑 = 𝑐 → ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) )
12	9 11	oveq12d	⊢ ( 𝑑 = 𝑐 → ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
13	12	cbvmptv	⊢ ( 𝑑 ∈ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } ↦ ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) ) = ( 𝑐 ∈ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
14	8 13	clwlkclwwlkf1o	⊢ ( 𝐺 ∈ USPGraph → ( 𝑑 ∈ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } ↦ ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) ) : { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } –1-1-onto→ ( ClWWalks ‘ 𝐺 ) )
15	14	adantr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑑 ∈ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } ↦ ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) ) : { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } –1-1-onto→ ( ClWWalks ‘ 𝐺 ) )
16		2fveq3	⊢ ( 𝑤 = 𝑠 → ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) )
17	16	breq2d	⊢ ( 𝑤 = 𝑠 → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) ↔ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) ) )
18	17	cbvrabv	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } = { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) }
19	18	mpteq1i	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) = ( 𝑐 ∈ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
20		fveq2	⊢ ( 𝑐 = 𝑑 → ( 2^nd ‘ 𝑐 ) = ( 2^nd ‘ 𝑑 ) )
21		2fveq3	⊢ ( 𝑐 = 𝑑 → ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) = ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) )
22	21	oveq1d	⊢ ( 𝑐 = 𝑑 → ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) )
23	20 22	oveq12d	⊢ ( 𝑐 = 𝑑 → ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) )
24	23	cbvmptv	⊢ ( 𝑐 ∈ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) = ( 𝑑 ∈ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } ↦ ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) )
25	19 24	eqtri	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) = ( 𝑑 ∈ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } ↦ ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) )
26	25	a1i	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) = ( 𝑑 ∈ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } ↦ ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) ) )
27	8	eqcomi	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } = { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) }
28	27	a1i	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } = { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } )
29		eqidd	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ClWWalks ‘ 𝐺 ) = ( ClWWalks ‘ 𝐺 ) )
30	26 28 29	f1oeq123d	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } –1-1-onto→ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝑑 ∈ { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } ↦ ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) ) : { 𝑠 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑠 ) ) } –1-1-onto→ ( ClWWalks ‘ 𝐺 ) ) )
31	15 30	mpbird	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } –1-1-onto→ ( ClWWalks ‘ 𝐺 ) )
32		fveq2	⊢ ( 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) )
33	32	3ad2ant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∧ 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) )
34		2fveq3	⊢ ( 𝑤 = 𝑐 → ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) )
35	34	breq2d	⊢ ( 𝑤 = 𝑐 → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) ↔ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
36	35	elrab	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↔ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
37		clwlknf1oclwwlknlem1	⊢ ( ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) → ( ♯ ‘ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) = ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) )
38	36 37	sylbi	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } → ( ♯ ‘ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) = ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) )
39	38	3ad2ant2	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∧ 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) → ( ♯ ‘ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) = ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) )
40	33 39	eqtrd	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∧ 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) )
41	40	eqeq1d	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∧ 𝑠 = ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) → ( ( ♯ ‘ 𝑠 ) = 𝑁 ↔ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) )
42	5 31 41	f1oresrab	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) ↾ { 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } ) : { 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } –1-1-onto→ { 𝑠 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑠 ) = 𝑁 } )
43	1 2 3 4	clwlknf1oclwwlknlem3	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → 𝐹 = ( ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) ) ↾ 𝐶 ) )
44	2	a1i	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ) → 𝐵 = ( 2^nd ‘ 𝑐 ) )
45		clwlkwlk	⊢ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) → 𝑐 ∈ ( Walks ‘ 𝐺 ) )
46		wlkcpr	⊢ ( 𝑐 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) )
47	1	fveq2i	⊢ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( 1^st ‘ 𝑐 ) )
48		wlklenvm1	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) )
49	47 48	eqtrid	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) )
50	46 49	sylbi	⊢ ( 𝑐 ∈ ( Walks ‘ 𝐺 ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) )
51	45 50	syl	⊢ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) )
52	51	adantr	⊢ ( ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) )
53	36 52	sylbi	⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) )
54	53	adantl	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) )
55	44 54	oveq12d	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ) → ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
56	55	mpteq2dva	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) ) = ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) )
57	34	eqeq1d	⊢ ( 𝑤 = 𝑐 → ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ↔ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) )
58	57	cbvrabv	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 }
59		nnge1	⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
60		breq2	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ↔ 1 ≤ 𝑁 ) )
61	59 60	syl5ibrcom	⊢ ( 𝑁 ∈ ℕ → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
62	61	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
63	62	adantr	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
64	63	pm4.71rd	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ↔ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) ) )
65	64	rabbidva	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) } )
66	58 65	eqtrid	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) } )
67	36	anbi1i	⊢ ( ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) ↔ ( ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) )
68		anass	⊢ ( ( ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) ↔ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) ) )
69	67 68	bitri	⊢ ( ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) ↔ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) ) )
70	69	rabbia2	⊢ { 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) }
71	66 3 70	3eqtr4g	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → 𝐶 = { 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } )
72	56 71	reseq12d	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) ) ↾ 𝐶 ) = ( ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) ↾ { 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } ) )
73	43 72	eqtrd	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → 𝐹 = ( ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) ↾ { 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } ) )
74		clwlknf1oclwwlknlem2	⊢ ( 𝑁 ∈ ℕ → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) } )
75	74	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) } )
76	75 3 70	3eqtr4g	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → 𝐶 = { 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } )
77		clwwlkn	⊢ ( 𝑁 ClWWalksN 𝐺 ) = { 𝑠 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑠 ) = 𝑁 }
78	77	a1i	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ClWWalksN 𝐺 ) = { 𝑠 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑠 ) = 𝑁 } )
79	73 76 78	f1oeq123d	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( 𝐹 : 𝐶 –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ) ↾ { 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } ) : { 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } –1-1-onto→ { 𝑠 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑠 ) = 𝑁 } ) )
80	42 79	mpbird	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → 𝐹 : 𝐶 –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) )

Metamath Proof Explorer

Theorem clwlknf1oclwwlkn

Proof