Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
|- ( g = G -> ( WWalks ` g ) = ( WWalks ` G ) ) |
2 |
1
|
adantl |
|- ( ( n = N /\ g = G ) -> ( WWalks ` g ) = ( WWalks ` G ) ) |
3 |
|
oveq1 |
|- ( n = N -> ( n + 1 ) = ( N + 1 ) ) |
4 |
3
|
eqeq2d |
|- ( n = N -> ( ( # ` w ) = ( n + 1 ) <-> ( # ` w ) = ( N + 1 ) ) ) |
5 |
4
|
adantr |
|- ( ( n = N /\ g = G ) -> ( ( # ` w ) = ( n + 1 ) <-> ( # ` w ) = ( N + 1 ) ) ) |
6 |
2 5
|
rabeqbidv |
|- ( ( n = N /\ g = G ) -> { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) } = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } ) |
7 |
|
df-wwlksn |
|- WWalksN = ( n e. NN0 , g e. _V |-> { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) } ) |
8 |
|
fvex |
|- ( WWalks ` G ) e. _V |
9 |
8
|
rabex |
|- { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } e. _V |
10 |
6 7 9
|
ovmpoa |
|- ( ( N e. NN0 /\ G e. _V ) -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } ) |
11 |
10
|
expcom |
|- ( G e. _V -> ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } ) ) |
12 |
7
|
reldmmpo |
|- Rel dom WWalksN |
13 |
12
|
ovprc2 |
|- ( -. G e. _V -> ( N WWalksN G ) = (/) ) |
14 |
|
fvprc |
|- ( -. G e. _V -> ( WWalks ` G ) = (/) ) |
15 |
14
|
rabeqdv |
|- ( -. G e. _V -> { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } = { w e. (/) | ( # ` w ) = ( N + 1 ) } ) |
16 |
|
rab0 |
|- { w e. (/) | ( # ` w ) = ( N + 1 ) } = (/) |
17 |
15 16
|
eqtrdi |
|- ( -. G e. _V -> { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } = (/) ) |
18 |
13 17
|
eqtr4d |
|- ( -. G e. _V -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } ) |
19 |
18
|
a1d |
|- ( -. G e. _V -> ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } ) ) |
20 |
11 19
|
pm2.61i |
|- ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } ) |