Step | Hyp | Ref
| Expression |
1 | | ne0i 3737 |
. . 3
    2WalksOnOt       2WalksOnOt      |
2 | | df-ov 6293 |
. . . . 5
   2WalksOnOt
     2WalksOnOt
        |
3 | | ndmfv 5889 |
. . . . 5
     2WalksOnOt    2WalksOnOt          |
4 | 2, 3 | syl5eq 2497 |
. . . 4
     2WalksOnOt     2WalksOnOt      |
5 | 4 | necon1ai 2651 |
. . 3
    2WalksOnOt        2WalksOnOt    |
6 | | simpl 459 |
. . . . . . . . 9
 
   |
7 | | id 22 |
. . . . . . . . . . . . 13
   |
8 | 7, 7 | xpeq12d 4859 |
. . . . . . . . . . . 12
       |
9 | 8, 7 | xpeq12d 4859 |
. . . . . . . . . . 11
           |
10 | 9 | adantr 467 |
. . . . . . . . . 10
 
           |
11 | | oveq12 6299 |
. . . . . . . . . . . . . 14
 
  WalkOn   WalkOn    |
12 | 11 | oveqd 6307 |
. . . . . . . . . . . . 13
 
    WalkOn       WalkOn      |
13 | 12 | breqd 4413 |
. . . . . . . . . . . 12
 
      WalkOn    
    WalkOn        |
14 | 13 | 3anbi1d 1343 |
. . . . . . . . . . 11
 
       WalkOn                                         WalkOn                                       |
15 | 14 | 2exbidv 1770 |
. . . . . . . . . 10
 
           WalkOn                                             WalkOn                                       |
16 | 10, 15 | rabeqbidv 3040 |
. . . . . . . . 9
 
               WalkOn                                                   WalkOn                                       |
17 | 6, 6, 16 | mpt2eq123dv 6353 |
. . . . . . . 8
 
                 WalkOn                                       
              WalkOn                                        |
18 | | df-2wlkonot 25586 |
. . . . . . . 8
2WalksOnOt                   WalkOn                                        |
19 | 17, 18 | ovmpt2ga 6426 |
. . . . . . 7
 
                WalkOn                                        2WalksOnOt                  WalkOn                                        |
20 | 19 | dmeqd 5037 |
. . . . . 6
 
                WalkOn                                       
2WalksOnOt                  WalkOn                                        |
21 | 20 | eleq2d 2514 |
. . . . 5
 
                WalkOn                                            2WalksOnOt                     WalkOn                                         |
22 | | dmoprabss 6378 |
. . . . . . . . 9
     
                  WalkOn                                          |
23 | 22 | sseli 3428 |
. . . . . . . 8
  
      
                  WalkOn                                              |
24 | | opelxp 4864 |
. . . . . . . . . . . 12
  
       |
25 | | 2wlkonot 25593 |
. . . . . . . . . . . . . . 15
    
     2WalksOnOt                  WalkOn                                       |
26 | 25 | eleq2d 2514 |
. . . . . . . . . . . . . 14
    
  
  
2WalksOnOt   
              WalkOn                                        |
27 | | elrabi 3193 |
. . . . . . . . . . . . . . 15
               WalkOn                                           |
28 | | simpl 459 |
. . . . . . . . . . . . . . . . . 18
    
  
   |
29 | 28 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   


 
     
   |
30 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
    
  
   |
31 | 30 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   


 
     
   |
32 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
   


 
           |
33 | 29, 31, 32 | 3jca 1188 |
. . . . . . . . . . . . . . . 16
   


 
        

       |
34 | 33 | ex 436 |
. . . . . . . . . . . . . . 15
    
  
       

        |
35 | 27, 34 | syl5 33 |
. . . . . . . . . . . . . 14
    
  
              WalkOn                                        

        |
36 | 26, 35 | sylbid 219 |
. . . . . . . . . . . . 13
    
  
  
2WalksOnOt   
 
 

        |
37 | 36 | expcom 437 |
. . . . . . . . . . . 12
 
  

    2WalksOnOt       

         |
38 | 24, 37 | sylbi 199 |
. . . . . . . . . . 11
  
  
 
 
  
2WalksOnOt   
 
 

         |
39 | 38 | com12 32 |
. . . . . . . . . 10
 
       
  
2WalksOnOt   
 
 

         |
40 | 39 | 3adant3 1028 |
. . . . . . . . 9
 
                WalkOn                                            
    2WalksOnOt       

         |
41 | 40 | com12 32 |
. . . . . . . 8
  
  
 
                WalkOn                                           2WalksOnOt       

         |
42 | 23, 41 | syl 17 |
. . . . . . 7
  
      
                  WalkOn                                                         WalkOn                                           2WalksOnOt       

         |
43 | | df-mpt2 6295 |
. . . . . . . 8
                WalkOn                                              

              WalkOn                                        |
44 | 43 | dmeqi 5036 |
. . . . . . 7
                WalkOn                                            
 

              WalkOn                                        |
45 | 42, 44 | eleq2s 2547 |
. . . . . 6
  
                 WalkOn                                       
                WalkOn                                       
  
2WalksOnOt   
 
 

         |
46 | 45 | com12 32 |
. . . . 5
 
                WalkOn                                                           WalkOn                                          2WalksOnOt       

         |
47 | 21, 46 | sylbid 219 |
. . . 4
 
                WalkOn                                            2WalksOnOt      2WalksOnOt       

         |
48 | | 3ianor 1002 |
. . . . 5
   
              WalkOn                                      

                WalkOn                                         |
49 | | df-3or 986 |
. . . . . 6
                  WalkOn                                      
 

                WalkOn                                         |
50 | | ianor 491 |
. . . . . . . 8
       |
51 | 18 | mpt2ndm0 6510 |
. . . . . . . . . . . 12
    2WalksOnOt
   |
52 | 51 | dmeqd 5037 |
. . . . . . . . . . 11
    2WalksOnOt    |
53 | 52 | eleq2d 2514 |
. . . . . . . . . 10
        2WalksOnOt 
      |
54 | | dm0 5048 |
. . . . . . . . . . 11
 |
55 | 54 | eleq2i 2521 |
. . . . . . . . . 10
  
      |
56 | 53, 55 | syl6bb 265 |
. . . . . . . . 9
        2WalksOnOt 
      |
57 | | noel 3735 |
. . . . . . . . . 10
    |
58 | 57 | pm2.21i 135 |
. . . . . . . . 9
  
     2WalksOnOt       

        |
59 | 56, 58 | syl6bi 232 |
. . . . . . . 8
        2WalksOnOt  
  
2WalksOnOt   
 
 

         |
60 | 50, 59 | sylbir 217 |
. . . . . . 7
        2WalksOnOt  
  
2WalksOnOt   
 
 

         |
61 | | anor 492 |
. . . . . . . . 9
 
 
   |
62 | | id 22 |
. . . . . . . . . . . . 13
   |
63 | 62 | ancri 555 |
. . . . . . . . . . . 12
 
   |
64 | 63 | adantr 467 |
. . . . . . . . . . 11
 
     |
65 | | mpt2exga 6869 |
. . . . . . . . . . 11
 
  
              WalkOn                                        |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
 
  
              WalkOn                                        |
67 | 66 | pm2.24d 138 |
. . . . . . . . 9
 
                  WalkOn                                           2WalksOnOt      2WalksOnOt       

          |
68 | 61, 67 | sylbir 217 |
. . . . . . . 8
 
   
              WalkOn                                           2WalksOnOt  
  
2WalksOnOt   
 
 

          |
69 | 68 | imp 431 |
. . . . . . 7
     
              WalkOn                                            2WalksOnOt      2WalksOnOt       

         |
70 | 60, 69 | jaoi3 981 |
. . . . . 6
  
  
              WalkOn                                            2WalksOnOt      2WalksOnOt       

         |
71 | 49, 70 | sylbi 199 |
. . . . 5
                  WalkOn                                            2WalksOnOt      2WalksOnOt       

         |
72 | 48, 71 | sylbi 199 |
. . . 4
   
              WalkOn                                            2WalksOnOt      2WalksOnOt       

         |
73 | 47, 72 | pm2.61i 168 |
. . 3
  
  2WalksOnOt      2WalksOnOt       

        |
74 | 1, 5, 73 | 3syl 18 |
. 2
    2WalksOnOt        2WalksOnOt       

        |
75 | 74 | pm2.43i 49 |
1
    2WalksOnOt       

       |