Step |
Hyp |
Ref |
Expression |
1 |
|
wrdnfi |
|- ( ( Vtx ` G ) e. Fin -> { w e. Word ( Vtx ` G ) | ( # ` w ) = ( N + 1 ) } e. Fin ) |
2 |
|
simpr |
|- ( ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) -> ( # ` w ) = ( N + 1 ) ) |
3 |
2
|
a1i |
|- ( w e. Word ( Vtx ` G ) -> ( ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) -> ( # ` w ) = ( N + 1 ) ) ) |
4 |
3
|
ss2rabi |
|- { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } C_ { w e. Word ( Vtx ` G ) | ( # ` w ) = ( N + 1 ) } |
5 |
4
|
a1i |
|- ( ( Vtx ` G ) e. Fin -> { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } C_ { w e. Word ( Vtx ` G ) | ( # ` w ) = ( N + 1 ) } ) |
6 |
1 5
|
ssfid |
|- ( ( Vtx ` G ) e. Fin -> { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } e. Fin ) |
7 |
|
wwlksn |
|- ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } ) |
8 |
|
df-rab |
|- { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } = { w | ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) } |
9 |
7 8
|
eqtrdi |
|- ( N e. NN0 -> ( N WWalksN G ) = { w | ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) } ) |
10 |
|
3anan12 |
|- ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( w e. Word ( Vtx ` G ) /\ ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) |
11 |
10
|
anbi1i |
|- ( ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) <-> ( ( w e. Word ( Vtx ` G ) /\ ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ ( # ` w ) = ( N + 1 ) ) ) |
12 |
|
anass |
|- ( ( ( w e. Word ( Vtx ` G ) /\ ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ ( # ` w ) = ( N + 1 ) ) <-> ( w e. Word ( Vtx ` G ) /\ ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) ) ) |
13 |
11 12
|
bitri |
|- ( ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) <-> ( w e. Word ( Vtx ` G ) /\ ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) ) ) |
14 |
13
|
abbii |
|- { w | ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } = { w | ( w e. Word ( Vtx ` G ) /\ ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) ) } |
15 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
16 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
17 |
15 16
|
iswwlks |
|- ( w e. ( WWalks ` G ) <-> ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) |
18 |
17
|
anbi1i |
|- ( ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) <-> ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) ) |
19 |
18
|
abbii |
|- { w | ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) } = { w | ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } |
20 |
|
df-rab |
|- { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } = { w | ( w e. Word ( Vtx ` G ) /\ ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) ) } |
21 |
14 19 20
|
3eqtr4i |
|- { w | ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) } = { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } |
22 |
9 21
|
eqtrdi |
|- ( N e. NN0 -> ( N WWalksN G ) = { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } ) |
23 |
22
|
eleq1d |
|- ( N e. NN0 -> ( ( N WWalksN G ) e. Fin <-> { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } e. Fin ) ) |
24 |
6 23
|
imbitrrid |
|- ( N e. NN0 -> ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin ) ) |
25 |
|
df-nel |
|- ( N e/ NN0 <-> -. N e. NN0 ) |
26 |
25
|
biimpri |
|- ( -. N e. NN0 -> N e/ NN0 ) |
27 |
26
|
olcd |
|- ( -. N e. NN0 -> ( G e/ _V \/ N e/ NN0 ) ) |
28 |
|
wwlksnndef |
|- ( ( G e/ _V \/ N e/ NN0 ) -> ( N WWalksN G ) = (/) ) |
29 |
27 28
|
syl |
|- ( -. N e. NN0 -> ( N WWalksN G ) = (/) ) |
30 |
|
0fin |
|- (/) e. Fin |
31 |
29 30
|
eqeltrdi |
|- ( -. N e. NN0 -> ( N WWalksN G ) e. Fin ) |
32 |
31
|
a1d |
|- ( -. N e. NN0 -> ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin ) ) |
33 |
24 32
|
pm2.61i |
|- ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin ) |