Step | Hyp | Ref
| Expression |
1 | | simp1 1008 |
. . . . . . 7
  USGrph
    
USGrph   |
2 | | uzuzle23 11199 |
. . . . . . . . 9
    
      |
3 | | uznn0sub 11190 |
. . . . . . . . 9
    
    |
4 | 2, 3 | syl 17 |
. . . . . . . 8
    
    |
5 | 4 | 3ad2ant3 1031 |
. . . . . . 7
  USGrph
    
    |
6 | | simp2 1009 |
. . . . . . 7
  USGrph
    
  |
7 | | numclwwlk.c |
. . . . . . . 8
   ClWWalksN       |
8 | | numclwwlk.f |
. . . . . . . 8
 

           |
9 | 7, 8 | numclwwlkovfel2 25811 |
. . . . . . 7
  USGrph


 
     
 
Word 
 ..^                      lastS                        |
10 | 1, 5, 6, 9 | syl3anc 1268 |
. . . . . 6
  USGrph
    
         Word 
 ..^                      lastS                        |
11 | | ccatws1cl 12753 |
. . . . . . . . . . . . . . . . 17
  Word
  ++      Word   |
12 | 11 | ex 436 |
. . . . . . . . . . . . . . . 16
 Word 
 ++     
Word    |
13 | 12 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . 15
  Word   ..^                      lastS          
 ++     
Word    |
14 | 13 | 3ad2ant1 1029 |
. . . . . . . . . . . . . 14
   Word   ..^                      lastS         
             ++      Word    |
15 | 14 | com12 32 |
. . . . . . . . . . . . 13
    Word   ..^                      lastS                      ++      Word    |
16 | 15 | 3ad2ant2 1030 |
. . . . . . . . . . . 12
  USGrph
    
   Word   ..^                      lastS         
            ++      Word    |
17 | 16 | imp 431 |
. . . . . . . . . . 11
   USGrph
       Word   ..^                      lastS                       ++      Word   |
18 | 17 | adantr 467 |
. . . . . . . . . 10
    USGrph
       Word 
 ..^                      lastS                          Neighbors    ++     
Word   |
19 | | nbgraisvtx 25159 |
. . . . . . . . . . . . . 14
 USGrph      Neighbors     |
20 | | s1cl 12741 |
. . . . . . . . . . . . . 14
     Word
  |
21 | 19, 20 | syl6 34 |
. . . . . . . . . . . . 13
 USGrph      Neighbors      Word
   |
22 | 21 | 3ad2ant1 1029 |
. . . . . . . . . . . 12
  USGrph
    
     Neighbors      Word
   |
23 | 22 | adantr 467 |
. . . . . . . . . . 11
   USGrph
       Word   ..^                      lastS                           Neighbors      Word
   |
24 | 23 | imp 431 |
. . . . . . . . . 10
    USGrph
       Word 
 ..^                      lastS                          Neighbors       Word
  |
25 | | ccatcl 12720 |
. . . . . . . . . 10
   ++      Word     Word    ++      ++     
Word   |
26 | 18, 24, 25 | syl2anc 667 |
. . . . . . . . 9
    USGrph
       Word 
 ..^                      lastS                          Neighbors     ++      ++      Word   |
27 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  Word  lastS          Word   |
28 | 27 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       Neighbors 
 Word  lastS                       
Word   |
29 | 28 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         Neighbors  
Word  lastS                        
USGrph
       ..^       
Word   |
30 | | elfzonn0 11960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ..^      
  |
31 | 30 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         Neighbors  
Word  lastS                        
USGrph
       ..^       
  |
32 | | lencl 12687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 Word       |
33 | | elfzo0 11956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  ..^       
               |
34 | | nn0re 10878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36

  |
35 | 34 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
         |
36 | | nn0re 10878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
      |
37 | | peano2rem 9941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
        |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    
        |
39 | 38 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
               |
40 | 36 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
             |
41 | 35, 39, 40 | 3jca 1188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                     |
42 | 36 | ltm1d 10539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    
            |
43 | 42 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                   |
44 | | lttr 9710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                       |
45 | 44 | expcomd 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       
               |
46 | 41, 43, 45 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
             
       |
47 | 46 | impancom 442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
             
       |
48 | 47 | 3adant2 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
            |
49 | 33, 48 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  ..^      
            |
50 | 32, 49 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 Word   ..^      
       |
51 | 50 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
 Neighbors 
 Word  lastS             ..^      
       |
52 | 51 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        Neighbors  
Word  lastS                        
USGrph
        ..^      
       |
53 | 52 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         Neighbors  
Word  lastS                        
USGrph
       ..^       
      |
54 | 29, 31, 53 | 3jca 1188 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         Neighbors  
Word  lastS                        
USGrph
       ..^       
 Word
       |
55 | 6 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        Neighbors  
Word  lastS                        
USGrph
        |
56 | 19 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  USGrph
    
     Neighbors     |
57 | 56 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     Neighbors    USGrph
    
   |
58 | 57 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       Neighbors 
 Word  lastS                          USGrph
        |
59 | 58 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        Neighbors  
Word  lastS                        
USGrph
        |
60 | 55, 59 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        Neighbors  
Word  lastS                        
USGrph
      
   |
61 | 60 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         Neighbors  
Word  lastS                        
USGrph
       ..^       

   |
62 | | ccat2s1fvw 12771 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   Word
     
     ++      ++               |
63 | 62 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   Word
     
         ++     
++           |
64 | 54, 61, 63 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         Neighbors  
Word  lastS                        
USGrph
       ..^       
       ++      ++           |
65 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  Word
 ..^        Word   |
66 | | peano2nn0 10910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

    |
67 | 66 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
              
    |
68 | 33, 67 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  ..^      
    |
69 | 68 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  Word
 ..^            |
70 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
         |
71 | 35, 70, 40 | ltaddsubd 10213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
             
         |
72 | 71 | biimprd 227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                       |
73 | 72 | impancom 442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             
         |
74 | 73 | 3adant2 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
              
              |
75 | 33, 74 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  ..^      
              |
76 | 32, 75 | mpan9 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  Word
 ..^                |
77 | 65, 69, 76 | 3jca 1188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  Word
 ..^        
Word  
         |
78 | 77 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 Word   ..^      
 Word  
          |
79 | 78 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
 Neighbors 
 Word  lastS             ..^      
 Word  
          |
80 | 79 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        Neighbors  
Word  lastS                        
USGrph
        ..^      
 Word  
          |
81 | 80 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         Neighbors  
Word  lastS                        
USGrph
       ..^       
 Word  
         |
82 | | ccat2s1fvw 12771 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   Word          
     ++      ++                   |
83 | 81, 61, 82 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         Neighbors  
Word  lastS                        
USGrph
       ..^       
   ++      ++                   |
84 | 83 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         Neighbors  
Word  lastS                        
USGrph
       ..^       
         ++      ++             |
85 | 64, 84 | preq12d 4059 |
. . . . . . . . . . . . . . . . . . . . . . 23
         Neighbors  
Word  lastS                        
USGrph
       ..^       
                 ++     
++             ++      ++              |
86 | 85 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . 22
         Neighbors  
Word  lastS                        
USGrph
       ..^       
             
    ++      ++             ++     
++               |
87 | 86 | ralbidva 2824 |
. . . . . . . . . . . . . . . . . . . . 21
        Neighbors  
Word  lastS                        
USGrph
       
 ..^                       ..^            ++      ++             ++     
++               |
88 | 87 | biimpd 211 |
. . . . . . . . . . . . . . . . . . . 20
        Neighbors  
Word  lastS                        
USGrph
       
 ..^                    
  ..^            ++     
++             ++      ++               |
89 | 88 | exp41 615 |
. . . . . . . . . . . . . . . . . . 19
     Neighbors    Word  lastS                         USGrph
        ..^                       ..^            ++      ++             ++     
++                  |
90 | 89 | com15 96 |
. . . . . . . . . . . . . . . . . 18
 
 ..^                       Word  lastS         
               USGrph
          Neighbors 
  ..^            ++     
++             ++      ++                  |
91 | 90 | expd 438 |
. . . . . . . . . . . . . . . . 17
 
 ..^                      Word   lastS                     
  USGrph     
     Neighbors    ..^            ++     
++             ++      ++                   |
92 | 91 | com12 32 |
. . . . . . . . . . . . . . . 16
 Word  
 ..^                    
  lastS                        USGrph
          Neighbors 
  ..^            ++     
++             ++      ++                   |
93 | 92 | 3imp 1202 |
. . . . . . . . . . . . . . 15
  Word   ..^                      lastS                         USGrph
          Neighbors 
  ..^            ++     
++             ++      ++                 |
94 | 93 | 3impib 1206 |
. . . . . . . . . . . . . 14
   Word   ..^                      lastS         
             USGrph
          Neighbors    ..^            ++     
++             ++      ++                |
95 | 94 | impcom 432 |
. . . . . . . . . . . . 13
   USGrph
       Word   ..^                      lastS                           Neighbors    ..^            ++     
++             ++      ++               |
96 | 95 | imp 431 |
. . . . . . . . . . . 12
    USGrph
       Word 
 ..^                      lastS                          Neighbors     ..^            ++     
++             ++      ++              |
97 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   Word             Word   |
98 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                   |
99 | 98 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
                 |
100 | | eluzelcn 11170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
  |
101 | | 2cnd 10682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
  |
102 | | 1cnd 9659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
  |
103 | 100, 101,
102 | subsub4d 10017 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
 
        |
104 | | 2p1e3 10733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
    |
106 | 105 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
        |
107 | | uznn0sub 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
    |
108 | 106, 107 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
      |
109 | 103, 108 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
 
    |
110 | 109 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
           |
111 | 99, 110 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
             |
112 | 111 | adantll 720 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   Word                     |
113 | 32, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 Word             |
114 | 113 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   Word                         |
115 | 97, 112, 114 | 3jca 1188 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   Word              Word                    |
116 | 115 | exp31 609 |
. . . . . . . . . . . . . . . . . . . . . . 23
 Word        
    
Word      
               |
117 | 116 | a1dd 47 |
. . . . . . . . . . . . . . . . . . . . . 22
 Word                   Word      
                |
118 | 117 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . 21
  Word   ..^                      lastS                     
      Word      
                |
119 | 118 | 3imp 1202 |
. . . . . . . . . . . . . . . . . . . 20
   Word   ..^                      lastS         
                 Word      
              |
120 | 119 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
    
   Word   ..^                      lastS         
            Word      
              |
121 | 120 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . . . 18
  USGrph
    
   Word   ..^                      lastS         
            Word      
              |
122 | 121 | imp 431 |
. . . . . . . . . . . . . . . . 17
   USGrph
       Word   ..^                      lastS                       Word                    |
123 | 122 | adantr 467 |
. . . . . . . . . . . . . . . 16
    USGrph
       Word 
 ..^                      lastS                          Neighbors   
Word      
             |
124 | 19 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . . . . 23
  Word 
USGrph        Neighbors 
   |
125 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  USGrph
   |
126 | 125 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
  Word 
USGrph  
  |
127 | 124, 126 | jctild 546 |
. . . . . . . . . . . . . . . . . . . . . 22
  Word 
USGrph        Neighbors 

    |
128 | 127 | ex 436 |
. . . . . . . . . . . . . . . . . . . . 21
 Word   USGrph
      Neighbors 

     |
129 | 128 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . 20
  Word   ..^                      lastS            USGrph 
     Neighbors  
     |
130 | 129 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . 19
   Word   ..^                      lastS         
             USGrph

     Neighbors  
     |
131 | 130 | com12 32 |
. . . . . . . . . . . . . . . . . 18
  USGrph
    Word   ..^                      lastS                          Neighbors 

     |
132 | 131 | 3adant3 1028 |
. . . . . . . . . . . . . . . . 17
  USGrph
    
   Word   ..^                      lastS         
                Neighbors 

     |
133 | 132 | imp31 434 |
. . . . . . . . . . . . . . . 16
    USGrph
       Word 
 ..^                      lastS                          Neighbors   
   |
134 | | ccat2s1fvw 12771 |
. . . . . . . . . . . . . . . 16
   Word      
                 ++      ++                           |
135 | 123, 133,
134 | syl2anc 667 |
. . . . . . . . . . . . . . 15
    USGrph
       Word 
 ..^                      lastS                          Neighbors      ++      ++                           |
136 | | nn0cn 10879 |
. . . . . . . . . . . . . . . . . . . . . 22
    
      |
137 | | ax-1cn 9597 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
138 | | npcan 9884 |
. . . . . . . . . . . . . . . . . . . . . 22
     
               |
139 | 136, 137,
138 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . . 21
    
              |
140 | 32, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 Word               |
141 | 140 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . 19
  Word   ..^                      lastS                        |
142 | 141 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . 18
   Word   ..^                      lastS         
                         |
143 | 142 | ad2antlr 733 |
. . . . . . . . . . . . . . . . 17
    USGrph
       Word 
 ..^                      lastS                          Neighbors                 |
144 | 143 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
    USGrph
       Word 
 ..^                      lastS                          Neighbors      ++      ++                    ++      ++               |
145 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   USGrph

Word  Word   |
146 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   USGrph

Word            |
147 | 145, 146 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   USGrph

Word   Word            |
148 | 147 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    USGrph

Word      Neighbors    Word            |
149 | 125 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    USGrph

Word      Neighbors  
  |
150 | 19 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   USGrph

Word       Neighbors     |
151 | 150 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    USGrph

Word      Neighbors  
  |
152 | | ccatw2s1p1 12769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   Word          
     ++      ++               |
153 | 148, 149,
151, 152 | syl12anc 1266 |
. . . . . . . . . . . . . . . . . . . . . . 23
    USGrph

Word      Neighbors      ++      ++               |
154 | 153 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . 22
   USGrph

Word       Neighbors     ++      ++                |
155 | 154 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . 21
 Word   USGrph
      Neighbors 
   ++      ++                 |
156 | 155 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . 20
  Word   ..^                      lastS            USGrph 
     Neighbors     ++      ++                 |
157 | 156 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . 19
   Word   ..^                      lastS         
             USGrph

     Neighbors     ++      ++                 |
158 | 157 | com12 32 |
. . . . . . . . . . . . . . . . . 18
  USGrph
    Word   ..^                      lastS                          Neighbors 
   ++      ++                 |
159 | 158 | 3adant3 1028 |
. . . . . . . . . . . . . . . . 17
  USGrph
    
   Word   ..^                      lastS         
                Neighbors 
   ++      ++                 |
160 | 159 | imp31 434 |
. . . . . . . . . . . . . . . 16
    USGrph
       Word 
 ..^                      lastS                          Neighbors      ++      ++               |
161 | 144, 160 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
    USGrph
       Word 
 ..^                      lastS                          Neighbors      ++      ++                   |
162 | 135, 161 | preq12d 4059 |
. . . . . . . . . . . . . 14
    USGrph
       Word 
 ..^                      lastS                          Neighbors       ++      ++                   ++      ++                                 |
163 | | lsw 12711 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 Word lastS               |
164 | 163 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
Word  lastS               |
165 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
Word        |
166 | 164, 165 | preq12d 4059 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
Word   lastS                        |
167 | 166 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . 22
     
Word    lastS        
                |
168 | 167 | biimpd 211 |
. . . . . . . . . . . . . . . . . . . . 21
     
Word    lastS                         |
169 | 168 | ex 436 |
. . . . . . . . . . . . . . . . . . . 20
     
Word  
lastS        
                 |
170 | 169 | com3l 84 |
. . . . . . . . . . . . . . . . . . 19
 Word  
lastS        
    
                 |
171 | 170 | imp 431 |
. . . . . . . . . . . . . . . . . 18
  Word  lastS                               |
172 | 171 | 3adant2 1027 |
. . . . . . . . . . . . . . . . 17
  Word   ..^                      lastS              
                |
173 | 172 | a1d 26 |
. . . . . . . . . . . . . . . 16
  Word   ..^                      lastS                     
                 |
174 | 173 | 3imp 1202 |
. . . . . . . . . . . . . . 15
   Word   ..^                      lastS         
                          |
175 | 174 | ad2antlr 733 |
. . . . . . . . . . . . . 14
    USGrph
       Word 
 ..^                      lastS                          Neighbors                  |
176 | 162, 175 | eqeltrd 2529 |
. . . . . . . . . . . . 13
    USGrph
       Word 
 ..^                      lastS                          Neighbors       ++      ++                   ++      ++                    |
177 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
178 | 177, 152 | mpanl2 687 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  Word 
     ++      ++               |
179 | | ccatw2s1p2 12770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   Word          
     ++      ++                 |
180 | 177, 179 | mpanl2 687 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  Word 
     ++      ++                 |
181 | 178, 180 | preq12d 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  Word 
      ++      ++                 ++      ++                     |
182 | 181 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  Word     ++     
++                 ++     
++                      |
183 | 182 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 Word     ++     
++                 ++     
++                       |
184 | 19, 183 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . 22
 USGrph      Neighbors  
 Word     ++     
++                 ++     
++                        |
185 | 184 | com24 90 |
. . . . . . . . . . . . . . . . . . . . 21
 USGrph  Word 
     Neighbors      ++      ++                 ++      ++                        |
186 | 185 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
 Word  USGrph

     Neighbors      ++      ++                 ++      ++                        |
187 | 186 | impd 433 |
. . . . . . . . . . . . . . . . . . 19
 Word   USGrph
      Neighbors 
    ++      ++                 ++      ++                       |
188 | 187 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . 18
  Word   ..^                      lastS            USGrph 
     Neighbors      ++      ++                 ++      ++                       |
189 | 188 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . 17
   Word   ..^                      lastS         
             USGrph

     Neighbors      ++      ++                 ++      ++                       |
190 | 189 | com12 32 |
. . . . . . . . . . . . . . . 16
  USGrph
    Word   ..^                      lastS                          Neighbors 
    ++      ++                 ++      ++                       |
191 | 190 | 3adant3 1028 |
. . . . . . . . . . . . . . 15
  USGrph
    
   Word   ..^                      lastS         
                Neighbors 
    ++      ++                 ++      ++                       |
192 | 191 | imp31 434 |
. . . . . . . . . . . . . 14
    USGrph
       Word 
 ..^                      lastS                          Neighbors       ++      ++                 ++      ++                     |
193 | | nbgraeledg 25158 |
. . . . . . . . . . . . . . . . . 18
 USGrph      Neighbors 
      |
194 | | prcom 4050 |
. . . . . . . . . . . . . . . . . . . 20
    
  |
195 | 194 | eleq1i 2520 |
. . . . . . . . . . . . . . . . . . 19
   
     |
196 | 195 | biimpi 198 |
. . . . . . . . . . . . . . . . . 18
         |
197 | 193, 196 | syl6bi 232 |
. . . . . . . . . . . . . . . . 17
 USGrph      Neighbors        |
198 | 197 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . 16
  USGrph
    
     Neighbors        |
199 | 198 | adantr 467 |
. . . . . . . . . . . . . . 15
   USGrph
       Word   ..^                      lastS                           Neighbors        |
200 | 199 | imp 431 |
. . . . . . . . . . . . . 14
    USGrph
       Word 
 ..^                      lastS                          Neighbors        |
201 | 192, 200 | eqeltrd 2529 |
. . . . . . . . . . . . 13
    USGrph
       Word 
 ..^                      lastS                          Neighbors       ++      ++                 ++      ++                  |
202 | | ovex 6318 |
. . . . . . . . . . . . . 14
       |
203 | | fvex 5875 |
. . . . . . . . . . . . . 14
     |
204 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
      
   ++      ++            ++      ++                 |
205 | | oveq1 6297 |
. . . . . . . . . . . . . . . . 17
      
            |
206 | 205 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
      
   ++      ++              ++      ++                   |
207 | 204, 206 | preq12d 4059 |
. . . . . . . . . . . . . . 15
      
    ++      ++             ++     
++                ++      ++                   ++     
++                    |
208 | 207 | eleq1d 2513 |
. . . . . . . . . . . . . 14
      
     ++      ++             ++     
++                ++     
++                   ++     
++                     |
209 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
    
   ++      ++            ++      ++               |
210 | | oveq1 6297 |
. . . . . . . . . . . . . . . . 17
    
          |
211 | 210 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
    
   ++      ++              ++      ++                 |
212 | 209, 211 | preq12d 4059 |
. . . . . . . . . . . . . . 15
    
    ++      ++             ++     
++                ++      ++                 ++      ++                  |
213 | 212 | eleq1d 2513 |
. . . . . . . . . . . . . 14
    
     ++      ++             ++     
++                ++     
++                 ++     
++                   |
214 | 202, 203,
208, 213 | ralpr 4025 |
. . . . . . . . . . . . 13
 
                 ++      ++             ++     
++                 ++      ++                   ++     
++                      ++     
++                 ++     
++                   |
215 | 176, 201,
214 | sylanbrc 670 |
. . . . . . . . . . . 12
    USGrph
       Word 
 ..^                      lastS                          Neighbors                     ++      ++             ++     
++              |
216 | 96, 215 | jca 535 |
. . . . . . . . . . 11
    USGrph
       Word 
 ..^                      lastS                          Neighbors    
 ..^            ++      ++             ++     
++                              ++      ++             ++     
++               |
217 | | 2cnd 10682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
  |
218 | | 1cnd 9659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
  |
219 | 136, 217,
218 | 3jca 1188 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
        |
220 | 32, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 Word         |
221 | 220 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  Word   ..^                      lastS              
   |
222 | 221 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
   Word   ..^                      lastS         
                     |
223 | | addsubass 9885 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
              |