Step | Hyp | Ref
| Expression |
1 | | ne0i 3728 |
. . 3
    2SPathOnOt       2SPathOnOt      |
2 | | df-ov 6311 |
. . . . 5
   2SPathOnOt
     2SPathOnOt
        |
3 | | ndmfv 5903 |
. . . . 5
     2SPathOnOt    2SPathOnOt          |
4 | 2, 3 | syl5eq 2517 |
. . . 4
     2SPathOnOt     2SPathOnOt      |
5 | 4 | necon1ai 2670 |
. . 3
    2SPathOnOt        2SPathOnOt    |
6 | | simpl 464 |
. . . . . . . . 9
 
   |
7 | | id 22 |
. . . . . . . . . . . . 13
   |
8 | 7, 7 | xpeq12d 4864 |
. . . . . . . . . . . 12
       |
9 | 8, 7 | xpeq12d 4864 |
. . . . . . . . . . 11
           |
10 | 9 | adantr 472 |
. . . . . . . . . 10
 
           |
11 | | oveq12 6317 |
. . . . . . . . . . . . . 14
 
  SPathOn   SPathOn    |
12 | 11 | oveqd 6325 |
. . . . . . . . . . . . 13
 
    SPathOn       SPathOn      |
13 | 12 | breqd 4406 |
. . . . . . . . . . . 12
 
      SPathOn    
    SPathOn        |
14 | 13 | 3anbi1d 1369 |
. . . . . . . . . . 11
 
       SPathOn                                         SPathOn                                       |
15 | 14 | 2exbidv 1778 |
. . . . . . . . . 10
 
           SPathOn                                             SPathOn
                                      |
16 | 10, 15 | rabeqbidv 3026 |
. . . . . . . . 9
 
               SPathOn                                                   SPathOn
                                      |
17 | 6, 6, 16 | mpt2eq123dv 6372 |
. . . . . . . 8
 
                 SPathOn                                       
              SPathOn                                        |
18 | | df-2spthonot 25667 |
. . . . . . . 8
2SPathOnOt                   SPathOn                                        |
19 | 17, 18 | ovmpt2ga 6445 |
. . . . . . 7
 
                SPathOn
                                       2SPathOnOt                  SPathOn
                                       |
20 | 19 | dmeqd 5042 |
. . . . . 6
 
                SPathOn
                                      
2SPathOnOt                  SPathOn                                        |
21 | 20 | eleq2d 2534 |
. . . . 5
 
                SPathOn
                                           2SPathOnOt                     SPathOn                                         |
22 | | dmoprabss 6397 |
. . . . . . . . 9
     
                  SPathOn                                          |
23 | 22 | sseli 3414 |
. . . . . . . 8
  
      
                  SPathOn                                              |
24 | | opelxp 4869 |
. . . . . . . . . . . 12
  
       |
25 | | 2spthonot 25673 |
. . . . . . . . . . . . . . 15
    
     2SPathOnOt                  SPathOn
                                      |
26 | 25 | eleq2d 2534 |
. . . . . . . . . . . . . 14
    
  
  
2SPathOnOt   
              SPathOn                                        |
27 | | elrabi 3181 |
. . . . . . . . . . . . . . 15
               SPathOn                                           |
28 | | simpl 464 |
. . . . . . . . . . . . . . . . . 18
    
  
   |
29 | 28 | adantr 472 |
. . . . . . . . . . . . . . . . 17
   


 
     
   |
30 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
    
  
   |
31 | 30 | adantr 472 |
. . . . . . . . . . . . . . . . 17
   


 
     
   |
32 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
   


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


 
        

       |
34 | 33 | ex 441 |
. . . . . . . . . . . . . . 15
    
  
       

        |
35 | 27, 34 | syl5 32 |
. . . . . . . . . . . . . 14
    
  
              SPathOn                                        

        |
36 | 26, 35 | sylbid 223 |
. . . . . . . . . . . . 13
    
  
  
2SPathOnOt   
 
 

        |
37 | 36 | expcom 442 |
. . . . . . . . . . . 12
 
  

    2SPathOnOt       

         |
38 | 24, 37 | sylbi 200 |
. . . . . . . . . . 11
  
  
 
 
  
2SPathOnOt   
 
 

         |
39 | 38 | com12 31 |
. . . . . . . . . 10
 
       
  
2SPathOnOt   
 
 

         |
40 | 39 | 3adant3 1050 |
. . . . . . . . 9
 
                SPathOn
                                           
    2SPathOnOt       

         |
41 | 40 | com12 31 |
. . . . . . . 8
  
  
 
                SPathOn                                           2SPathOnOt       

         |
42 | 23, 41 | syl 17 |
. . . . . . 7
  
      
                  SPathOn                                                         SPathOn                                           2SPathOnOt       

         |
43 | | df-mpt2 6313 |
. . . . . . . 8
                SPathOn                                              

              SPathOn                                        |
44 | 43 | dmeqi 5041 |
. . . . . . 7
                SPathOn
                                           
 

              SPathOn
                                       |
45 | 42, 44 | eleq2s 2567 |
. . . . . 6
  
                 SPathOn                                       
                SPathOn                                       
  
2SPathOnOt   
 
 

         |
46 | 45 | com12 31 |
. . . . 5
 
                SPathOn
                                                          SPathOn                                          2SPathOnOt       

         |
47 | 21, 46 | sylbid 223 |
. . . 4
 
                SPathOn
                                           2SPathOnOt      2SPathOnOt       

         |
48 | | 3ianor 1024 |
. . . . 5
   
              SPathOn                                      

                SPathOn                                         |
49 | | df-3or 1008 |
. . . . . 6
                  SPathOn                                      
 

                SPathOn
                                        |
50 | | ianor 496 |
. . . . . . . 8
       |
51 | 18 | mpt2ndm0 6529 |
. . . . . . . . . . . 12
    2SPathOnOt
   |
52 | 51 | dmeqd 5042 |
. . . . . . . . . . 11
    2SPathOnOt    |
53 | 52 | eleq2d 2534 |
. . . . . . . . . 10
        2SPathOnOt 
      |
54 | | dm0 5054 |
. . . . . . . . . . 11
 |
55 | 54 | eleq2i 2541 |
. . . . . . . . . 10
  
      |
56 | 53, 55 | syl6bb 269 |
. . . . . . . . 9
        2SPathOnOt 
      |
57 | | noel 3726 |
. . . . . . . . . 10
    |
58 | 57 | pm2.21i 136 |
. . . . . . . . 9
  
     2SPathOnOt       

        |
59 | 56, 58 | syl6bi 236 |
. . . . . . . 8
        2SPathOnOt  
  
2SPathOnOt   
 
 

         |
60 | 50, 59 | sylbir 218 |
. . . . . . 7
        2SPathOnOt  
  
2SPathOnOt   
 
 

         |
61 | | anor 497 |
. . . . . . . . 9
 
 
   |
62 | | id 22 |
. . . . . . . . . . . . 13
   |
63 | 62 | ancri 561 |
. . . . . . . . . . . 12
 
   |
64 | 63 | adantr 472 |
. . . . . . . . . . 11
 
     |
65 | | mpt2exga 6888 |
. . . . . . . . . . 11
 
  
              SPathOn                                        |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
 
  
              SPathOn                                        |
67 | 66 | pm2.24d 139 |
. . . . . . . . 9
 
                  SPathOn                                           2SPathOnOt      2SPathOnOt       

          |
68 | 61, 67 | sylbir 218 |
. . . . . . . 8
 
   
              SPathOn                                           2SPathOnOt  
  
2SPathOnOt   
 
 

          |
69 | 68 | imp 436 |
. . . . . . 7
     
              SPathOn                                            2SPathOnOt      2SPathOnOt       

         |
70 | 60, 69 | jaoi3 980 |
. . . . . 6
  
  
              SPathOn                                            2SPathOnOt      2SPathOnOt       

         |
71 | 49, 70 | sylbi 200 |
. . . . 5
                  SPathOn                                            2SPathOnOt      2SPathOnOt       

         |
72 | 48, 71 | sylbi 200 |
. . . 4
   
              SPathOn                                            2SPathOnOt      2SPathOnOt       

         |
73 | 47, 72 | pm2.61i 169 |
. . 3
  
  2SPathOnOt      2SPathOnOt       

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

        |
75 | 74 | pm2.43i 48 |
1
    2SPathOnOt       

       |