Step | Hyp | Ref
| Expression |
1 | | fvex 5801 |
. . . 4
  WWalksN    
   |
2 | 1 | a1i 11 |
. . 3
   WWalksN    
  WWalksN    
    |
3 | | rabexg 4542 |
. . 3
   WWalksN
         WWalksN
        substr      
 lastS    lastS        |
4 | | mptexg 6048 |
. . 3
    WWalksN    
    substr      
 lastS    lastS          WWalksN    
    substr      
 lastS    lastS      lastS      |
5 | 2, 3, 4 | 3syl 20 |
. 2
   WWalksN    
    WWalksN
        substr      
 lastS    lastS      lastS      |
6 | | eqid 2451 |
. . . 4
 Word         substr      
 lastS    lastS       Word
       
substr        lastS    lastS       |
7 | | preq2 4055 |
. . . . . 6
  lastS    
 lastS       |
8 | 7 | eleq1d 2520 |
. . . . 5
  
lastS      lastS        |
9 | 8 | cbvrabv 3069 |
. . . 4

 lastS      
 lastS       |
10 | | fveq2 5791 |
. . . . . . . 8
           |
11 | 10 | eqeq1d 2453 |
. . . . . . 7
       
         |
12 | | oveq1 6199 |
. . . . . . . 8
  substr      
 substr         |
13 | 12 | eqeq1d 2453 |
. . . . . . 7
   substr
       substr
         |
14 | | fveq2 5791 |
. . . . . . . . 9
 lastS   lastS     |
15 | 14 | preq2d 4061 |
. . . . . . . 8
  lastS    lastS    
lastS    lastS      |
16 | 15 | eleq1d 2520 |
. . . . . . 7
  
lastS    lastS    
lastS    lastS       |
17 | 11, 13, 16 | 3anbi123d 1290 |
. . . . . 6
         
substr        lastS    lastS             substr      
 lastS    lastS        |
18 | 17 | cbvrabv 3069 |
. . . . 5
 Word        
substr        lastS    lastS       Word
       
substr        lastS    lastS       |
19 | | mpteq1 4472 |
. . . . 5
  Word        
substr        lastS    lastS       Word
       
substr        lastS    lastS        Word        
substr        lastS    lastS      lastS      Word         substr      
 lastS    lastS      lastS      |
20 | 18, 19 | ax-mp 5 |
. . . 4
  Word
        substr        lastS   
lastS      lastS      Word         substr      
 lastS    lastS      lastS     |
21 | 6, 9, 20 | wwlkextbij0 30504 |
. . 3
   WWalksN    
  Word         substr  
     lastS   
lastS      lastS       Word
       
substr        lastS    lastS          lastS        |
22 | | eqid 2451 |
. . . . . . 7
 Word        
substr        lastS    lastS       Word
       
substr        lastS    lastS       |
23 | 22 | wwlkextwrd 30500 |
. . . . . 6
   WWalksN    
 Word         substr      
 lastS    lastS         WWalksN    
    substr      
 lastS    lastS        |
24 | 23 | eqcomd 2459 |
. . . . 5
   WWalksN    
   WWalksN         substr        lastS   
lastS       Word
       
substr        lastS    lastS        |
25 | 24 | mpteq1d 4473 |
. . . 4
   WWalksN    
    WWalksN
        substr      
 lastS    lastS      lastS      Word
       
substr        lastS    lastS      lastS      |
26 | 6 | wwlkextwrd 30500 |
. . . . 5
   WWalksN    
 Word         substr      
 lastS    lastS         WWalksN    
    substr      
 lastS    lastS        |
27 | 26 | eqcomd 2459 |
. . . 4
   WWalksN    
   WWalksN         substr        lastS   
lastS       Word
       
substr        lastS    lastS        |
28 | | eqidd 2452 |
. . . 4
   WWalksN    

 lastS      
 lastS        |
29 | 25, 27, 28 | f1oeq123d 5738 |
. . 3
   WWalksN    
     WWalksN    
    substr      
 lastS    lastS      lastS         WWalksN    
    substr      
 lastS    lastS          lastS     
  Word         substr  
     lastS   
lastS      lastS       Word
       
substr        lastS    lastS          lastS         |
30 | 21, 29 | mpbird 232 |
. 2
   WWalksN    
    WWalksN
        substr      
 lastS    lastS      lastS         WWalksN
        substr      
 lastS    lastS          lastS        |
31 | | f1oeq1 5732 |
. . 3
     WWalksN
        substr      
 lastS    lastS      lastS          WWalksN    
    substr      
 lastS    lastS          lastS     
    WWalksN
        substr      
 lastS    lastS      lastS         WWalksN
        substr      
 lastS    lastS          lastS         |
32 | 31 | spcegv 3156 |
. 2
     WWalksN    
    substr      
 lastS    lastS      lastS         WWalksN
        substr      
 lastS    lastS      lastS         WWalksN
        substr      
 lastS    lastS          lastS            WWalksN    
    substr      
 lastS    lastS          lastS         |
33 | 5, 30, 32 | sylc 60 |
1
   WWalksN    
      WWalksN         substr        lastS   
lastS          lastS        |