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