Step |
Hyp |
Ref |
Expression |
1 |
|
ovex |
|- ( N WWalksN G ) e. _V |
2 |
1
|
rabex |
|- { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } e. _V |
3 |
|
ovex |
|- ( N ClWWalksN G ) e. _V |
4 |
|
eqid |
|- { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |
5 |
|
eqid |
|- ( c e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |-> ( c prefix N ) ) = ( c e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |-> ( c prefix N ) ) |
6 |
4 5
|
clwwlkf1o |
|- ( N e. NN -> ( c e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |-> ( c prefix N ) ) : { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } -1-1-onto-> ( N ClWWalksN G ) ) |
7 |
|
f1oen2g |
|- ( ( { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } e. _V /\ ( N ClWWalksN G ) e. _V /\ ( c e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |-> ( c prefix N ) ) : { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } -1-1-onto-> ( N ClWWalksN G ) ) -> { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } ~~ ( N ClWWalksN G ) ) |
8 |
2 3 6 7
|
mp3an12i |
|- ( N e. NN -> { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } ~~ ( N ClWWalksN G ) ) |