This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐺 ) )