Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . . . 6
WWalksN |
2 | 1 | mptrabex 6488 |
. . . . 5
WWalksN
lastS substr |
3 | 2 | resex 5443 |
. . . 4
WWalksN
lastS substr WWalksN lastS |
4 | | eqid 2622 |
. . . . 5
WWalksN
lastS substr WWalksN
lastS substr |
5 | | eqid 2622 |
. . . . . 6
WWalksN
lastS
WWalksN lastS |
6 | 5, 4 | clwwlksf1o 26919 |
. . . . 5
WWalksN
lastS substr WWalksN lastS ClWWalksN
|
7 | | fveq1 6190 |
. . . . . . . 8
substr substr |
8 | 7 | eqeq1d 2624 |
. . . . . . 7
substr
substr |
9 | 8 | 3ad2ant3 1084 |
. . . . . 6
WWalksN
lastS
substr
substr |
10 | | fveq2 6191 |
. . . . . . . . . . . . 13
lastS lastS |
11 | | fveq1 6190 |
. . . . . . . . . . . . 13
|
12 | 10, 11 | eqeq12d 2637 |
. . . . . . . . . . . 12
lastS
lastS |
13 | 12 | elrab 3363 |
. . . . . . . . . . 11
WWalksN
lastS
WWalksN
lastS |
14 | | eqid 2622 |
. . . . . . . . . . . . . 14
Vtx Vtx |
15 | | eqid 2622 |
. . . . . . . . . . . . . 14
Edg Edg |
16 | 14, 15 | wwlknp 26734 |
. . . . . . . . . . . . 13
WWalksN
Word Vtx ..^ Edg |
17 | | simpll 790 |
. . . . . . . . . . . . . . . 16
Word Vtx Word Vtx |
18 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . 20
|
19 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . . 20
|
20 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . . . 20
|
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
|
22 | | elfz1end 12371 |
. . . . . . . . . . . . . . . . . . . 20
|
23 | 22 | biimpi 206 |
. . . . . . . . . . . . . . . . . . 19
|
24 | | fzss2 12381 |
. . . . . . . . . . . . . . . . . . . 20
|
25 | 24 | sselda 3603 |
. . . . . . . . . . . . . . . . . . 19
|
26 | 21, 23, 25 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Word Vtx
|
28 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 28 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 29 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
|
31 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word Vtx
|
32 | 27, 31 | mpbird 247 |
. . . . . . . . . . . . . . . 16
Word Vtx |
33 | 17, 32 | jca 554 |
. . . . . . . . . . . . . . 15
Word Vtx Word
Vtx
|
34 | 33 | ex 450 |
. . . . . . . . . . . . . 14
Word Vtx
Word Vtx |
35 | 34 | 3adant3 1081 |
. . . . . . . . . . . . 13
Word Vtx ..^ Edg Word Vtx |
36 | 16, 35 | syl 17 |
. . . . . . . . . . . 12
WWalksN
Word Vtx
|
37 | 36 | adantr 481 |
. . . . . . . . . . 11
WWalksN lastS
Word Vtx
|
38 | 13, 37 | sylbi 207 |
. . . . . . . . . 10
WWalksN
lastS Word Vtx |
39 | 38 | impcom 446 |
. . . . . . . . 9
WWalksN
lastS Word Vtx
|
40 | | swrd0fv0 13440 |
. . . . . . . . 9
Word Vtx
substr |
41 | 39, 40 | syl 17 |
. . . . . . . 8
WWalksN
lastS substr |
42 | 41 | eqeq1d 2624 |
. . . . . . 7
WWalksN
lastS substr
|
43 | 42 | 3adant3 1081 |
. . . . . 6
WWalksN
lastS
substr
substr
|
44 | 9, 43 | bitrd 268 |
. . . . 5
WWalksN
lastS
substr
|
45 | 4, 6, 44 | f1oresrab 6395 |
. . . 4
WWalksN lastS substr
WWalksN
lastS WWalksN lastS ClWWalksN |
46 | | f1oeq1 6127 |
. . . . 5
WWalksN
lastS substr WWalksN lastS WWalksN
lastS ClWWalksN
WWalksN
lastS substr WWalksN lastS WWalksN lastS ClWWalksN |
47 | 46 | spcegv 3294 |
. . . 4
WWalksN lastS substr
WWalksN
lastS WWalksN lastS substr
WWalksN
lastS WWalksN lastS ClWWalksN WWalksN
lastS ClWWalksN |
48 | 3, 45, 47 | mpsyl 68 |
. . 3
WWalksN lastS ClWWalksN |
49 | | fveq1 6190 |
. . . . . . 7
|
50 | 49 | eqeq1d 2624 |
. . . . . 6
|
51 | 50 | cbvrabv 3199 |
. . . . 5
ClWWalksN
ClWWalksN |
52 | | f1oeq3 6129 |
. . . . 5
ClWWalksN ClWWalksN WWalksN lastS ClWWalksN
WWalksN
lastS ClWWalksN |
53 | 51, 52 | mp1i 13 |
. . . 4
WWalksN lastS ClWWalksN
WWalksN
lastS ClWWalksN |
54 | 53 | exbidv 1850 |
. . 3
WWalksN
lastS ClWWalksN
WWalksN lastS ClWWalksN |
55 | 48, 54 | mpbird 247 |
. 2
WWalksN lastS ClWWalksN |
56 | | df-rab 2921 |
. . . . 5
WWalksN
lastS WWalksN
lastS |
57 | | anass 681 |
. . . . . . 7
WWalksN lastS
WWalksN
lastS |
58 | 57 | bicomi 214 |
. . . . . 6
WWalksN lastS
WWalksN lastS |
59 | 58 | abbii 2739 |
. . . . 5
WWalksN
lastS WWalksN lastS |
60 | 13 | bicomi 214 |
. . . . . . . 8
WWalksN lastS
WWalksN
lastS |
61 | 60 | anbi1i 731 |
. . . . . . 7
WWalksN lastS
WWalksN lastS |
62 | 61 | abbii 2739 |
. . . . . 6
WWalksN
lastS WWalksN
lastS |
63 | | df-rab 2921 |
. . . . . 6
WWalksN lastS WWalksN
lastS |
64 | 62, 63 | eqtr4i 2647 |
. . . . 5
WWalksN
lastS WWalksN
lastS |
65 | 56, 59, 64 | 3eqtri 2648 |
. . . 4
WWalksN
lastS WWalksN lastS |
66 | | f1oeq2 6128 |
. . . 4
WWalksN lastS
WWalksN
lastS WWalksN lastS ClWWalksN
WWalksN
lastS ClWWalksN |
67 | 65, 66 | mp1i 13 |
. . 3
WWalksN
lastS ClWWalksN
WWalksN
lastS ClWWalksN |
68 | 67 | exbidv 1850 |
. 2
WWalksN lastS ClWWalksN
WWalksN lastS ClWWalksN |
69 | 55, 68 | mpbird 247 |
1
WWalksN
lastS ClWWalksN |