Step | Hyp | Ref
| Expression |
1 | | 2wlkonot 25605 |
. . . 4
  


     2WalksOnOt                  WalkOn                                       |
2 | 1 | eleq2d 2516 |
. . 3
  


      2WalksOnOt   
              WalkOn                                        |
3 | | fveq2 5870 |
. . . . . . . . 9
           |
4 | 3 | fveq2d 5874 |
. . . . . . . 8
                   |
5 | 4 | eqeq1d 2455 |
. . . . . . 7
         
           |
6 | 3 | fveq2d 5874 |
. . . . . . . 8
                   |
7 | 6 | eqeq1d 2455 |
. . . . . . 7
             
               |
8 | | fveq2 5870 |
. . . . . . . 8
           |
9 | 8 | eqeq1d 2455 |
. . . . . . 7
     
       |
10 | 5, 7, 9 | 3anbi123d 1341 |
. . . . . 6
                                                         |
11 | 10 | 3anbi3d 1347 |
. . . . 5
       WalkOn                                         WalkOn                                       |
12 | 11 | 2exbidv 1772 |
. . . 4
           WalkOn                                             WalkOn                                       |
13 | 12 | elrab 3198 |
. . 3
               WalkOn                                    
    
         WalkOn                                       |
14 | 2, 13 | syl6bb 265 |
. 2
  


      2WalksOnOt   
    
         WalkOn                                        |
15 | | simpl 459 |
. . . . . . . . 9
  


  
   |
16 | | vex 3050 |
. . . . . . . . . . 11
 |
17 | | vex 3050 |
. . . . . . . . . . 11
 |
18 | 16, 17 | pm3.2i 457 |
. . . . . . . . . 10
   |
19 | 18 | a1i 11 |
. . . . . . . . 9
  


      |
20 | | simpr 463 |
. . . . . . . . 9
  


  
   |
21 | | iswlkon 25274 |
. . . . . . . . 9
  

  
 
     WalkOn        Walks                   |
22 | 15, 19, 20, 21 | syl3anc 1269 |
. . . . . . . 8
  


       WalkOn    
   Walks
 
                |
23 | 22 | 3anbi1d 1345 |
. . . . . . 7
  


        WalkOn                                        Walks                                                  |
24 | 23 | anbi2d 711 |
. . . . . 6
  


       
     WalkOn                                              Walks                                                   |
25 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
26 | 25 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
  


 
  |
27 | 26 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
     Walks                   
     |
28 | 27 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
      Walks                   
          |
29 | | el2wlkonotlem 25602 |
. . . . . . . . . . . . . . . . . . . . . . 23
    Walks              |
30 | 29 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . 22
   Walks  
    
       |
31 | 30 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . . . . . . 21
    Walks      
        
    
       |
32 | 31 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     Walks                   
               |
33 | 32 | imp 431 |
. . . . . . . . . . . . . . . . . . 19
      Walks                   
              |
34 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
35 | 34 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
  


 
  |
36 | 35 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
     Walks                   
     |
37 | 36 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
      Walks                   
          |
38 | | el2xptp0 6842 |
. . . . . . . . . . . . . . . . . . 19
     
      
                          
           |
39 | 28, 33, 37, 38 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . 18
      Walks                   
                                        
           |
40 | | oteq2 4179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                   |
41 | 40 | eqcoms 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                   |
42 | 41 | eqeq2d 2463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     
               |
43 | 42 | biimpcd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             
       |
44 | 43 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
             Walks             
       |
45 | 44 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           
   Walks                           
       |
46 | 45 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                    Walks                       
      |
47 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    Walks          Walks
    |
48 | 47 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             Walks           Walks     |
49 | 48 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           
   Walks                         Walks     |
50 | 49 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                    Walks                       
  Walks     |
51 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    Walks              |
52 | 51 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             Walks               |
53 | 52 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           
   Walks                             |
54 | 53 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                    Walks                       
      |
55 | | eqcom 2460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    
      |
56 | 55 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           |
57 | 56 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           
   Walks                             |
58 | 57 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                    Walks                       
      |
59 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                    Walks                       
      |
60 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
                   |
61 | 60 | eqeq1d 2455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
             
       |
62 | | eqcom 2460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
    
      |
63 | 62 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
           |
64 | 61, 63 | syl6bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                     |
65 | 64 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    Walks                        |
66 | 65 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
             Walks                         |
67 | 66 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
              Walks                 
      |
68 | 67 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           
   Walks                             |
69 | 68 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                    Walks                       
      |
70 | 58, 59, 69 | 3jca 1189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                    Walks                       
                |
71 | 50, 54, 70 | 3jca 1189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                    Walks                       
   Walks
 
                     |
72 | 46, 71 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                    Walks                       
        Walks                         |
73 | 72 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                    Walks                           
   Walks                          |
74 | 73 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     Walks       
                    Walks                       
       Walks       
   
   
          |
75 | 29, 74 | rspcimedv 3154 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    Walks                       Walks                        
       Walks                          |
76 | 75 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
   Walks                           Walks       

        Walks                          |
77 | 76 | exp41 615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             Walks                          Walks       

        Walks                             |
78 | 77 | com15 96 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    Walks            Walks                              

        Walks                             |
79 | 78 | pm2.43i 49 |
. . . . . . . . . . . . . . . . . . . . . . 23
    Walks                                
       Walks                            |
80 | 79 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . 22
   Walks  
    
             
         
        Walks                             |
81 | 80 | com24 90 |
. . . . . . . . . . . . . . . . . . . . 21
   Walks  
    
        
    
         
        Walks                             |
82 | 81 | 3imp 1203 |
. . . . . . . . . . . . . . . . . . . 20
    Walks      
        
    
         
        Walks                           |
83 | 82 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
     Walks                   
        
        

       Walks                           |
84 | 83 | imp 431 |
. . . . . . . . . . . . . . . . . 18
      Walks                   
        
        

       Walks                          |
85 | 39, 84 | sylbid 219 |
. . . . . . . . . . . . . . . . 17
      Walks                   
                                         

       Walks                          |
86 | 85 | ex 436 |
. . . . . . . . . . . . . . . 16
     Walks                   
                                         

       Walks                           |
87 | 86 | com23 81 |
. . . . . . . . . . . . . . 15
     Walks                   
                                         

       Walks                           |
88 | 87 | ex 436 |
. . . . . . . . . . . . . 14
    Walks      
        
  


       
                                

       Walks                            |
89 | 88 | com4t 88 |
. . . . . . . . . . . . 13
                                
    
    Walks      
        
  


  

       Walks                            |
90 | 89 | ex 436 |
. . . . . . . . . . . 12
                                         Walks               
  


  

       Walks                             |
91 | 90 | com14 91 |
. . . . . . . . . . 11
    Walks      
        
                                    
  


  

       Walks                             |
92 | 91 | com23 81 |
. . . . . . . . . 10
    Walks      
        
    
                               
  


  

       Walks                             |
93 | 92 | 3imp 1203 |
. . . . . . . . 9
     Walks                                              
    
  


  

       Walks                           |
94 | 93 | impcom 432 |
. . . . . . . 8
          Walks                                                    
 

        Walks                          |
95 | 94 | com12 32 |
. . . . . . 7
  


       
    Walks      
                                          
       Walks                          |
96 | 25 | adantr 467 |
. . . . . . . . . . . . . . . . 17
  

   |
97 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
  

   |
98 | 34 | adantr 467 |
. . . . . . . . . . . . . . . . 17
  

   |
99 | 96, 97, 98 | 3jca 1189 |
. . . . . . . . . . . . . . . 16
  

 
   |
100 | | otel3xp 4873 |
. . . . . . . . . . . . . . . 16
      
        |
101 | 99, 100 | sylan2 477 |
. . . . . . . . . . . . . . 15
          
      |
102 | 101 | ex 436 |
. . . . . . . . . . . . . 14
                 |
103 | 102 | adantr 467 |
. . . . . . . . . . . . 13
         Walks       
   
   
                   |
104 | 103 | com12 32 |
. . . . . . . . . . . 12
  

          Walks                      
       |
105 | 104 | adantll 721 |
. . . . . . . . . . 11
     
 
          Walks                      
       |
106 | 105 | imp 431 |
. . . . . . . . . 10
      
 
 
       Walks       
   
   
       
      |
107 | | id 22 |
. . . . . . . . . . . . . . 15
   Walks  
  Walks     |
108 | 107 | 3ad2ant1 1030 |
. . . . . . . . . . . . . 14
    Walks                        Walks     |
109 | 108 | adantl 468 |
. . . . . . . . . . . . 13
         Walks       
   
   
         Walks
    |
110 | 109 | adantl 468 |
. . . . . . . . . . . 12
      
 
 
       Walks       
   
   
          Walks     |
111 | | eqcom 2460 |
. . . . . . . . . . . . . . . . 17
    
      |
112 | 111 | biimpi 198 |
. . . . . . . . . . . . . . . 16
           |
113 | 112 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . 15
     
   
           |
114 | 113 | 3ad2ant3 1032 |
. . . . . . . . . . . . . 14
    Walks                            |
115 | 114 | adantl 468 |
. . . . . . . . . . . . 13
         Walks       
   
   
             |
116 | 115 | adantl 468 |
. . . . . . . . . . . 12
      
 
 
       Walks       
   
   
              |
117 | | eqcom 2460 |
. . . . . . . . . . . . . . . . . . 19
    
      |
118 | 117 | biimpi 198 |
. . . . . . . . . . . . . . . . . 18
           |
119 | 118 | 3ad2ant3 1032 |
. . . . . . . . . . . . . . . . 17
     
   
           |
120 | 119, 61 | syl5ibr 225 |
. . . . . . . . . . . . . . . 16
                   
           |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . 15
   Walks  
    
 
   
   
                 |
122 | 121 | 3imp 1203 |
. . . . . . . . . . . . . 14
    Walks                                |
123 | 122 | adantl 468 |
. . . . . . . . . . . . 13
         Walks       
   
   
                 |
124 | 123 | adantl 468 |
. . . . . . . . . . . 12
      
 
 
       Walks       
   
   
                  |
125 | 110, 116,
124 | 3jca 1189 |
. . . . . . . . . . 11
      
 
 
       Walks       
   
   
           Walks                  |
126 | | id 22 |
. . . . . . . . . . . . . 14
           |
127 | 126 | 3ad2ant2 1031 |
. . . . . . . . . . . . 13
    Walks                            |
128 | 127 | adantl 468 |
. . . . . . . . . . . 12
         Walks       
   
   
             |
129 | 128 | adantl 468 |
. . . . . . . . . . 11
      
 
 
       Walks       
   
   
              |
130 | 99 | adantll 721 |
. . . . . . . . . . . . . . . . 17
     
 
 
   |
131 | | oteqimp 6817 |
. . . . . . . . . . . . . . . . 17
      

                         |
132 | 130, 131 | syl5 33 |
. . . . . . . . . . . . . . . 16
          
 
                          |
133 | | eqeq2 2464 |
. . . . . . . . . . . . . . . . . 18
             
               |
134 | 133 | 3anbi2d 1346 |
. . . . . . . . . . . . . . . . 17
                                                         |
135 | 134 | imbi2d 318 |
. . . . . . . . . . . . . . . 16
         
 
                             


 
                               |
136 | 132, 135 | syl5ib 223 |
. . . . . . . . . . . . . . 15
     
       
 
                                 |
137 | 136 | 3ad2ant2 1031 |
. . . . . . . . . . . . . 14
     
   
         
     
 
                               |
138 | 137 | 3ad2ant3 1032 |
. . . . . . . . . . . . 13
    Walks                          
     
 
                               |
139 | 138 | impcom 432 |
. . . . . . . . . . . 12
         Walks       
   
   
            
 
                              |
140 | 139 | impcom 432 |
. . . . . . . . . . 11
      
 
 
       Walks       
   
   
                                    |
141 | 125, 129,
140 | 3jca 1189 |
. . . . . . . . . 10
      
 
 
       Walks       
   
   
            Walks                                                 |
142 | 106, 141 | jca 535 |
. . . . . . . . 9
      
 
 
       Walks       
   
   
                 Walks                                                  |
143 | 142 | ex 436 |
. . . . . . . 8
     
 
          Walks                                Walks                                                   |
144 | 143 | rexlimdva 2881 |
. . . . . . 7
  


        
   Walks                      
    
    Walks      
                                            |
145 | 95, 144 | impbid 194 |
. . . . . 6
  


       
    Walks      
                                         

       Walks                          |
146 | 24, 145 | bitrd 257 |
. . . . 5
  


       
     WalkOn                                     

       Walks                          |
147 | 146 | 2exbidv 1772 |
. . . 4
  


           
     WalkOn                                         

       Walks       
   
   
          |
148 | | 19.42vv 1838 |
. . . 4
               WalkOn                                    
    
         WalkOn                                       |
149 | | rexcom4 3069 |
. . . . 5
              Walks                         
          Walks                         |
150 | | rexcom4 3069 |
. . . . . 6
        
   Walks                         
        Walks                         |
151 | 150 | exbii 1720 |
. . . . 5
              Walks       
   
   
      
         
   Walks                         |
152 | 149, 151 | bitr2i 254 |
. . . 4
     

       Walks       
   
   
      

        
   Walks                         |
153 | 147, 148,
152 | 3bitr3g 291 |
. . 3
  


       
         WalkOn                                    

        
   Walks                          |
154 | | 19.42vv 1838 |
. . . 4
             Walks       
   
   
      
            Walks           
   
         |
155 | 154 | rexbii 2891 |
. . 3
              Walks                        
           Walks                         |
156 | 153, 155 | syl6bb 265 |
. 2
  


       
         WalkOn                                    

            Walks           
   
          |
157 | 14, 156 | bitrd 257 |
1
  


      2WalksOnOt   

            Walks           
   
          |