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 ≤ ( ♯ ‘ ( 1st𝑤 ) ) } ≈ ( ClWWalks ‘ 𝐺 ) )

Proof

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