Step |
Hyp |
Ref |
Expression |
1 |
|
wwlkbp.v |
|- V = ( Vtx ` G ) |
2 |
|
df-wwlksn |
|- WWalksN = ( n e. NN0 , g e. _V |-> { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) } ) |
3 |
2
|
elmpocl |
|- ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ G e. _V ) ) |
4 |
|
simpl |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) ) -> ( N e. NN0 /\ G e. _V ) ) |
5 |
4
|
ancomd |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) ) -> ( G e. _V /\ N e. NN0 ) ) |
6 |
|
iswwlksn |
|- ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) ) |
7 |
6
|
adantr |
|- ( ( N e. NN0 /\ G e. _V ) -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) ) |
8 |
1
|
wwlkbp |
|- ( W e. ( WWalks ` G ) -> ( G e. _V /\ W e. Word V ) ) |
9 |
8
|
simprd |
|- ( W e. ( WWalks ` G ) -> W e. Word V ) |
10 |
9
|
adantr |
|- ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> W e. Word V ) |
11 |
7 10
|
syl6bi |
|- ( ( N e. NN0 /\ G e. _V ) -> ( W e. ( N WWalksN G ) -> W e. Word V ) ) |
12 |
11
|
imp |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) ) -> W e. Word V ) |
13 |
|
df-3an |
|- ( ( G e. _V /\ N e. NN0 /\ W e. Word V ) <-> ( ( G e. _V /\ N e. NN0 ) /\ W e. Word V ) ) |
14 |
5 12 13
|
sylanbrc |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) ) |
15 |
3 14
|
mpancom |
|- ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) ) |