Metamath Proof Explorer

Theorem clwlkclwwlken

Description: The set of the nonempty closed walks and the set of closed walks as word are equinumerous in a simple pseudograph. (Contributed by AV, 25-May-2022) (Proof shortened by AV, 4-Nov-2022)

		Ref	Expression
	Assertion	clwlkclwwlken	⊢ ( 𝐺 ∈ USPGraph → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ≈ ( ClWWalks ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( ClWalks ‘ 𝐺 ) ∈ V
2	1	rabex	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∈ V
3		fvex	⊢ ( ClWWalks ‘ 𝐺 ) ∈ V
4		2fveq3	⊢ ( 𝑤 = 𝑢 → ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑢 ) ) )
5	4	breq2d	⊢ ( 𝑤 = 𝑢 → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) ↔ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑢 ) ) ) )
6	5	cbvrabv	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } = { 𝑢 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑢 ) ) }
7		fveq2	⊢ ( 𝑑 = 𝑐 → ( 2^nd ‘ 𝑑 ) = ( 2^nd ‘ 𝑐 ) )
8		2fveq3	⊢ ( 𝑑 = 𝑐 → ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) = ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) )
9	8	oveq1d	⊢ ( 𝑑 = 𝑐 → ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) )
10	7 9	oveq12d	⊢ ( 𝑑 = 𝑐 → ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
11	10	cbvmptv	⊢ ( 𝑑 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) ) = ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
12	6 11	clwlkclwwlkf1o	⊢ ( 𝐺 ∈ USPGraph → ( 𝑑 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } –1-1-onto→ ( ClWWalks ‘ 𝐺 ) )
13		f1oen2g	⊢ ( ( { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ∈ V ∧ ( ClWWalks ‘ 𝐺 ) ∈ V ∧ ( 𝑑 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ↦ ( ( 2^nd ‘ 𝑑 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑑 ) ) − 1 ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } –1-1-onto→ ( ClWWalks ‘ 𝐺 ) ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ≈ ( ClWWalks ‘ 𝐺 ) )
14	2 3 12 13	mp3an12i	⊢ ( 𝐺 ∈ USPGraph → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) } ≈ ( ClWWalks ‘ 𝐺 ) )