Step | Hyp | Ref
| Expression |
1 | | simp1 988 |
. . . . . . . . . 10
  USGrph
    
USGrph   |
2 | | uzuzle23 30342 |
. . . . . . . . . . . 12
    
      |
3 | | uznn0sub 11004 |
. . . . . . . . . . . 12
    
    |
4 | 2, 3 | syl 16 |
. . . . . . . . . . 11
    
    |
5 | 4 | 3ad2ant3 1011 |
. . . . . . . . . 10
  USGrph
    
    |
6 | | simp2 989 |
. . . . . . . . . 10
  USGrph
    
  |
7 | | numclwwlk.c |
. . . . . . . . . . 11
   ClWWalksN       |
8 | | numclwwlk.f |
. . . . . . . . . . 11
 

           |
9 | 7, 8 | numclwwlkovfel2 30825 |
. . . . . . . . . 10
  USGrph


 
     
 
Word 
 ..^                      lastS                        |
10 | 1, 5, 6, 9 | syl3anc 1219 |
. . . . . . . . 9
  USGrph
    
         Word 
 ..^                      lastS                        |
11 | | simplll 757 |
. . . . . . . . . . . . . . . . 17
     USGrph
       Word             
    Neighbors           USGrph        |
12 | | simpr 461 |
. . . . . . . . . . . . . . . . . 18
    USGrph
       Word             
    Neighbors  
    Neighbors    |
13 | 12 | adantr 465 |
. . . . . . . . . . . . . . . . 17
     USGrph
       Word             
    Neighbors              Neighbors    |
14 | | simpr 461 |
. . . . . . . . . . . . . . . . 17
     USGrph
       Word             
    Neighbors                  |
15 | 7, 8 | numclwwlkovf2ex 30828 |
. . . . . . . . . . . . . . . . 17
   USGrph
    
    Neighbors        
  concat     
concat            |
16 | 11, 13, 14, 15 | syl3anc 1219 |
. . . . . . . . . . . . . . . 16
     USGrph
       Word             
    Neighbors            concat
     concat
           |
17 | | nbgraisvtx 23495 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 USGrph      Neighbors     |
18 | 17 | 3ad2ant1 1009 |
. . . . . . . . . . . . . . . . . . . . . . 23
  USGrph
    
     Neighbors     |
19 | 18 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . 22
   USGrph
       Word              
    Neighbors     |
20 | | simplll 757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    Word         USGrph
       Word   |
21 | | s1cl 12412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     Word
  |
22 | 21 | 3ad2ant2 1010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  USGrph
    
    Word
  |
23 | 22 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   Word         USGrph
     
    Word
  |
24 | 23 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    Word         USGrph
           Word
  |
25 | | s1cl 12412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     Word
  |
26 | 25 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    Word         USGrph
           Word
  |
27 | | ccatass 12405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  Word     Word     Word
   concat      concat
      concat      concat         |
28 | 27 | oveq1d 6216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  Word     Word     Word
    concat      concat     
substr         concat      concat      
substr         |
29 | 20, 24, 26, 28 | syl3anc 1219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    Word         USGrph
          concat      concat
     substr
        concat      concat      
substr         |
30 | | ccatcl 12393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      Word     Word
      concat     
Word   |
31 | 23, 25, 30 | syl2an 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    Word         USGrph
            concat     
Word   |
32 | | simpr 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  Word                |
33 | 32 | eqcomd 2462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  Word                |
34 | 33 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   Word         USGrph
     
        |
35 | 34 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    Word         USGrph
       
       |
36 | | swrdccatid 12507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  Word      concat     
Word 
        concat
     concat       substr  
      |
37 | 20, 31, 35, 36 | syl3anc 1219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    Word         USGrph
         concat
     concat       substr  
      |
38 | 29, 37 | eqtr2d 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    Word         USGrph
          concat     
concat      substr
        |
39 | 38 | exp31 604 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  Word          USGrph
     
   concat      concat     
substr           |
40 | 39 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . 23
   Word            
  USGrph     

   concat      concat     
substr           |
41 | 40 | impcom 430 |
. . . . . . . . . . . . . . . . . . . . . 22
   USGrph
       Word              
   concat     
concat      substr
         |
42 | 19, 41 | syld 44 |
. . . . . . . . . . . . . . . . . . . . 21
   USGrph
       Word              
    Neighbors     concat      concat
     substr
         |
43 | 42 | imp 429 |
. . . . . . . . . . . . . . . . . . . 20
    USGrph
       Word             
    Neighbors  
   concat      concat     
substr         |
44 | 43 | eleq1d 2523 |
. . . . . . . . . . . . . . . . . . 19
    USGrph
       Word             
    Neighbors  
          concat     
concat      substr
               |
45 | 44 | biimpd 207 |
. . . . . . . . . . . . . . . . . 18
    USGrph
       Word             
    Neighbors  
      
   concat
     concat
     substr
               |
46 | 45 | imp 429 |
. . . . . . . . . . . . . . . . 17
     USGrph
       Word             
    Neighbors             concat      concat
     substr
              |
47 | | simplrl 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    USGrph
       Word             
  Word          |
48 | 6 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   USGrph
       Word                |
49 | 48 | anim1i 568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    USGrph
       Word             
 
   |
50 | 47, 49 | jca 532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    USGrph
       Word             
   Word             |
51 | | ccatw2s1p2 30419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   Word              concat      concat               |
52 | 50, 51 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    USGrph
       Word             
    concat      concat               |
53 | | eluzelcn 10984 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
  |
54 | | 2cnd 10506 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
  |
55 | | ax-1cn 9452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
  |
57 | | subsub 9751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
 
         |
58 | 57 | eqcomd 2462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
           |
59 | 53, 54, 56, 58 | syl3anc 1219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
 
        |
60 | | 2m1e1 10548 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
    |
62 | 61 | oveq2d 6217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
        |
63 | 59, 62 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
 
      |
64 | 63 | 3ad2ant3 1011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  USGrph
    
 
      |
65 | 64 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   USGrph
       Word                      |
66 | 65 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    USGrph
       Word             
         |
67 | 66 | fveq2d 5804 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    USGrph
       Word             
    concat      concat                concat     
concat        
    |
68 | 52, 67 | eqtr3d 2497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    USGrph
       Word             
    concat      concat
       
    |
69 | 68 | ex 434 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   USGrph
       Word              
   concat     
concat        
     |
70 | 19, 69 | syld 44 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   USGrph
       Word              
    Neighbors     concat      concat
       
     |
71 | 70 | impcom 430 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
 Neighbors 
  USGrph     
 
Word                  concat      concat
       
    |
72 | 71 | eleq1d 2523 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 Neighbors 
  USGrph     
 
Word                    Neighbors 
   concat
     concat
       
    
 Neighbors     |
73 | 72 | biimpd 207 |
. . . . . . . . . . . . . . . . . . . . 21
    
 Neighbors 
  USGrph     
 
Word                    Neighbors     concat      concat
       
    
 Neighbors     |
74 | 73 | ex 434 |
. . . . . . . . . . . . . . . . . . . 20
     Neighbors     USGrph
       Word                   Neighbors 
   concat
     concat
       
    
 Neighbors      |
75 | 74 | pm2.43a 49 |
. . . . . . . . . . . . . . . . . . 19
     Neighbors     USGrph
       Word                 concat      concat               Neighbors     |
76 | 75 | impcom 430 |
. . . . . . . . . . . . . . . . . 18
    USGrph
       Word             
    Neighbors  
   concat
     concat
       
    
 Neighbors    |
77 | 76 | adantr 465 |
. . . . . . . . . . . . . . . . 17
     USGrph
       Word             
    Neighbors             concat      concat
       
    
 Neighbors    |
78 | | ccatw2s1p1 30418 |
. . . . . . . . . . . . . . . . . . . . . 22
   Word              concat      concat             |
79 | 50, 78 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
    USGrph
       Word             
    concat      concat             |
80 | 79 | ex 434 |
. . . . . . . . . . . . . . . . . . . 20
   USGrph
       Word              
   concat      concat
       
     |
81 | 19, 80 | syld 44 |
. . . . . . . . . . . . . . . . . . 19
   USGrph
       Word              
    Neighbors     concat     
concat        
     |
82 | 81 | imp 429 |
. . . . . . . . . . . . . . . . . 18
    USGrph
       Word             
    Neighbors  
   concat
     concat
       
    |
83 | 82 | adantr 465 |
. . . . . . . . . . . . . . . . 17
     USGrph
       Word             
    Neighbors             concat      concat
       
    |
84 | 46, 77, 83 | 3jca 1168 |
. . . . . . . . . . . . . . . 16
     USGrph
       Word             
    Neighbors              concat      concat     
substr                concat     
concat        
    
 Neighbors 
   concat
     concat
       
     |
85 | 16, 84 | jca 532 |
. . . . . . . . . . . . . . 15
     USGrph
       Word             
    Neighbors             concat      concat
             concat      concat
     substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
      |
86 | 85 | exp31 604 |
. . . . . . . . . . . . . 14
   USGrph
       Word              
    Neighbors        
   concat
     concat
             concat      concat
     substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
        |
87 | 86 | expcom 435 |
. . . . . . . . . . . . 13
   Word            
  USGrph     
     Neighbors  
         concat      concat     
        concat     
concat      substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
         |
88 | 87 | exp31 604 |
. . . . . . . . . . . 12
 Word               USGrph
          Neighbors  
         concat      concat     
        concat     
concat      substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
           |
89 | 88 | 3ad2ant1 1009 |
. . . . . . . . . . 11
  Word   ..^                      lastS                     
  USGrph     
     Neighbors  
         concat      concat     
        concat     
concat      substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
           |
90 | 89 | 3imp 1182 |
. . . . . . . . . 10
   Word   ..^                      lastS         
             USGrph
          Neighbors  
         concat      concat     
        concat     
concat      substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
         |
91 | 90 | com12 31 |
. . . . . . . . 9
  USGrph
    
   Word   ..^                      lastS         
                Neighbors 
      
   concat
     concat
             concat      concat
     substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
         |
92 | 10, 91 | sylbid 215 |
. . . . . . . 8
  USGrph
    
      
     Neighbors  
         concat      concat     
        concat     
concat      substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
         |
93 | 92 | com14 88 |
. . . . . . 7
       
           Neighbors 
  USGrph     
   concat
     concat
             concat      concat
     substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
         |
94 | 93 | pm2.43i 47 |
. . . . . 6
       
    Neighbors    USGrph
        concat     
concat              concat      concat
     substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
        |
95 | 94 | imp 429 |
. . . . 5
       
    Neighbors  
  USGrph     
   concat
     concat
             concat      concat
     substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
       |
96 | 95 | impcom 430 |
. . . 4
   USGrph
     
     
    Neighbors       concat      concat
             concat      concat
     substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
      |
97 | | oveq1 6208 |
. . . . . . 7
   concat      concat     
 substr          concat      concat
     substr
        |
98 | 97 | eleq1d 2523 |
. . . . . 6
   concat      concat     
  substr      
     
   concat
     concat
     substr
               |
99 | | fveq1 5799 |
. . . . . . 7
   concat      concat     
         concat      concat             |
100 | 99 | eleq1d 2523 |
. . . . . 6
   concat      concat     
           Neighbors 
   concat
     concat
       
    
 Neighbors     |
101 | | fveq1 5799 |
. . . . . . 7
   concat      concat     
         concat      concat             |
102 | 101 | eqeq1d 2456 |
. . . . . 6
   concat      concat     
      
   concat
     concat
       
     |
103 | 98, 100, 102 | 3anbi123d 1290 |
. . . . 5
   concat      concat     
   substr                       Neighbors        
    concat      concat
     substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
      |
104 | 103 | elrab 3224 |
. . . 4
   concat      concat
            substr                       Neighbors             concat      concat     
        concat     
concat      substr
               concat     
concat        
    
 Neighbors 
   concat
     concat
       
      |
105 | 96, 104 | sylibr 212 |
. . 3
   USGrph
     
     
    Neighbors      concat
     concat
            substr                       Neighbors            |
106 | | numclwwlk.g |
. . . . 5
 
                 
          |
107 | 7, 8, 106 | extwwlkfab 30832 |
. . . 4
  USGrph
    
           substr                       Neighbors            |
108 | 107 | adantr 465 |
. . 3
   USGrph
     
     
    Neighbors               substr                
    
 Neighbors 
          |
109 | 105, 108 | eleqtrrd 2545 |
. 2
   USGrph
     
     
    Neighbors      concat
     concat
           |
110 | 109 | ex 434 |
1
  USGrph
    
 
     
    Neighbors  
  concat     
concat             |