Step |
Hyp |
Ref |
Expression |
1 |
|
ovex |
⊢ ( 𝑁 WWalksN 𝐺 ) ∈ V |
2 |
1
|
rabex |
⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ∈ V |
3 |
|
ovex |
⊢ ( 𝑁 ClWWalksN 𝐺 ) ∈ V |
4 |
|
eqid |
⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } |
5 |
|
eqid |
⊢ ( 𝑐 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ↦ ( 𝑐 prefix 𝑁 ) ) = ( 𝑐 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ↦ ( 𝑐 prefix 𝑁 ) ) |
6 |
4 5
|
clwwlkf1o |
⊢ ( 𝑁 ∈ ℕ → ( 𝑐 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ↦ ( 𝑐 prefix 𝑁 ) ) : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) ) |
7 |
|
f1oen2g |
⊢ ( ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ∈ V ∧ ( 𝑁 ClWWalksN 𝐺 ) ∈ V ∧ ( 𝑐 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ↦ ( 𝑐 prefix 𝑁 ) ) : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ≈ ( 𝑁 ClWWalksN 𝐺 ) ) |
8 |
2 3 6 7
|
mp3an12i |
⊢ ( 𝑁 ∈ ℕ → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) } ≈ ( 𝑁 ClWWalksN 𝐺 ) ) |