Proof of Theorem usg2spthonot0
Step | Hyp | Ref
| Expression |
1 | | ne0i 3737 |
. . . . 5
  
     2SPathOnOt
      2SPathOnOt      |
2 | | 2spontn0vne 25615 |
. . . . 5
    2SPathOnOt      |
3 | 1, 2 | syl 17 |
. . . 4
  
     2SPathOnOt
     |
4 | | simpl 459 |
. . . . . . . . . . 11
  USGrph

 
USGrph   |
5 | 4 | adantl 468 |
. . . . . . . . . 10
  
USGrph 
   USGrph   |
6 | | 3simpb 1006 |
. . . . . . . . . . . 12
 
 
   |
7 | 6 | adantl 468 |
. . . . . . . . . . 11
  USGrph

 

   |
8 | 7 | adantl 468 |
. . . . . . . . . 10
  
USGrph 
   
   |
9 | | simpl 459 |
. . . . . . . . . 10
  
USGrph 
     |
10 | | 2pthwlkonot 25613 |
. . . . . . . . . 10
  USGrph



  
2SPathOnOt       2WalksOnOt
     |
11 | 5, 8, 9, 10 | syl3anc 1268 |
. . . . . . . . 9
  
USGrph 
      2SPathOnOt       2WalksOnOt      |
12 | 11 | eleq2d 2514 |
. . . . . . . 8
  
USGrph 
           2SPathOnOt
  
  
    2WalksOnOt       |
13 | | usgrav 25065 |
. . . . . . . . . . . 12
 USGrph 
   |
14 | 13, 6 | anim12i 570 |
. . . . . . . . . . 11
  USGrph

 
 
 
    |
15 | 14 | adantl 468 |
. . . . . . . . . 10
  
USGrph 
      
    |
16 | | el2wlkonotot1 25602 |
. . . . . . . . . 10
    
          2WalksOnOt
  

  
    2WalksOnOt        |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
  
USGrph 
           2WalksOnOt
  

  
    2WalksOnOt        |
18 | | df-3an 987 |
. . . . . . . . 9
 
 
     2WalksOnOt
   
 
    
   2WalksOnOt       |
19 | 17, 18 | syl6bb 265 |
. . . . . . . 8
  
USGrph 
           2WalksOnOt
  
 
    
   2WalksOnOt        |
20 | 12, 19 | bitrd 257 |
. . . . . . 7
  
USGrph 
           2SPathOnOt
  
 
    
   2WalksOnOt        |
21 | | simpll 760 |
. . . . . . . . . . . . 13
       |
22 | | simpr 463 |
. . . . . . . . . . . . . 14
 
   |
23 | 22 | adantr 467 |
. . . . . . . . . . . . 13
       |
24 | | simpr 463 |
. . . . . . . . . . . . 13
       |
25 | 21, 23, 24 | 3jca 1188 |
. . . . . . . . . . . 12
     
   |
26 | 25 | ex 436 |
. . . . . . . . . . 11
 
       |
27 | 26 | adantr 467 |
. . . . . . . . . 10
      
    2WalksOnOt    


    |
28 | 27 | com12 32 |
. . . . . . . . 9
            2WalksOnOt    

    |
29 | 28 | adantr 467 |
. . . . . . . 8
  
USGrph 
              2WalksOnOt    

    |
30 | 5 | adantl 468 |
. . . . . . . . . . . 12
      USGrph 
   
USGrph   |
31 | | simprrr 775 |
. . . . . . . . . . . . 13
      USGrph 
   

   |
32 | | eleq1 2517 |
. . . . . . . . . . . . . . . 16
 
   |
33 | 32 | adantr 467 |
. . . . . . . . . . . . . . 15
 
     |
34 | | eleq1 2517 |
. . . . . . . . . . . . . . . 16
 
   |
35 | 34 | adantl 468 |
. . . . . . . . . . . . . . 15
 
     |
36 | 33, 35 | 3anbi13d 1341 |
. . . . . . . . . . . . . 14
 
   

    |
37 | 36 | adantr 467 |
. . . . . . . . . . . . 13
      USGrph 
   
 
 
    |
38 | 31, 37 | mpbird 236 |
. . . . . . . . . . . 12
      USGrph 
   

   |
39 | | usg2wlkonot 25611 |
. . . . . . . . . . . 12
  USGrph

 
        2WalksOnOt       
  
    |
40 | 30, 38, 39 | syl2anc 667 |
. . . . . . . . . . 11
      USGrph 
   
        2WalksOnOt       
  
    |
41 | | preq1 4051 |
. . . . . . . . . . . . . . . 16
     
   |
42 | 41 | adantr 467 |
. . . . . . . . . . . . . . 15
 
   
     |
43 | 42 | eleq1d 2513 |
. . . . . . . . . . . . . 14
 
    
      |
44 | | preq2 4052 |
. . . . . . . . . . . . . . . 16
     
   |
45 | 44 | adantl 468 |
. . . . . . . . . . . . . . 15
 
   
     |
46 | 45 | eleq1d 2513 |
. . . . . . . . . . . . . 14
 
    
      |
47 | 43, 46 | anbi12d 717 |
. . . . . . . . . . . . 13
 
        
       
    |
48 | 47 | biimpd 211 |
. . . . . . . . . . . 12
 
        

  
  
     |
49 | 48 | adantr 467 |
. . . . . . . . . . 11
      USGrph 
   
      
     
  
    |
50 | 40, 49 | sylbid 219 |
. . . . . . . . . 10
      USGrph 
   
        2WalksOnOt          
    |
51 | 50 | impancom 442 |
. . . . . . . . 9
      
    2WalksOnOt    
   USGrph 
         
    |
52 | 51 | com12 32 |
. . . . . . . 8
  
USGrph 
              2WalksOnOt    
  
  
     |
53 | 29, 52 | jcad 536 |
. . . . . . 7
  
USGrph 
              2WalksOnOt    
 
    
        |
54 | 20, 53 | sylbid 219 |
. . . . . 6
  
USGrph 
           2SPathOnOt
     
  
  
      |
55 | 54 | ex 436 |
. . . . 5
   USGrph

          2SPathOnOt
     
  
  
       |
56 | 55 | com23 81 |
. . . 4
         2SPathOnOt
     USGrph

    
  
  
       |
57 | 3, 56 | mpcom 37 |
. . 3
  
     2SPathOnOt
     USGrph

    
  
  
      |
58 | 57 | com12 32 |
. 2
  USGrph

 
        2SPathOnOt     
      
      |
59 | | simpll 760 |
. . . . . . . 8
   USGrph 
  
  USGrph
  |
60 | | eleq1 2517 |
. . . . . . . . . . . . . . 15
 
   |
61 | 60 | eqcoms 2459 |
. . . . . . . . . . . . . 14
 
   |
62 | 61 | adantr 467 |
. . . . . . . . . . . . 13
 
     |
63 | | eleq1 2517 |
. . . . . . . . . . . . . . 15
 
   |
64 | 63 | eqcoms 2459 |
. . . . . . . . . . . . . 14
 
   |
65 | 64 | adantl 468 |
. . . . . . . . . . . . 13
 
     |
66 | 62, 65 | 3anbi13d 1341 |
. . . . . . . . . . . 12
 
   

    |
67 | 66 | biimpd 211 |
. . . . . . . . . . 11
 
    
    |
68 | 67 | adantld 469 |
. . . . . . . . . 10
 
   USGrph 
  
    |
69 | 68 | 3adant3 1028 |
. . . . . . . . 9
 
   USGrph 
  
    |
70 | 69 | impcom 432 |
. . . . . . . 8
   USGrph 
  
      |
71 | 59, 70, 39 | syl2anc 667 |
. . . . . . 7
   USGrph 
  
     
    2WalksOnOt       
  
    |
72 | 47 | 3adant3 1028 |
. . . . . . . 8
 
        
       
    |
73 | 72 | adantl 468 |
. . . . . . 7
   USGrph 
  
        
 
  
  
     |
74 | 71, 73 | bitr2d 258 |
. . . . . 6
   USGrph 
  
        
 
  
    2WalksOnOt       |
75 | 74 | pm5.32da 647 |
. . . . 5
  USGrph

 
   
  
  
             2WalksOnOt        |
76 | | df-3an 987 |
. . . . . . . 8
 

 

   |
77 | | ancom 452 |
. . . . . . . 8
    
      |
78 | 76, 77 | bitri 253 |
. . . . . . 7
 

      |
79 | 78 | anbi1i 701 |
. . . . . 6
   
  
    2WalksOnOt       
 
  
    2WalksOnOt       |
80 | | anass 655 |
. . . . . 6
             2WalksOnOt     
 
    
   2WalksOnOt        |
81 | 18 | bicomi 206 |
. . . . . . 7
      
    2WalksOnOt        
    2WalksOnOt       |
82 | 81 | anbi2i 700 |
. . . . . 6
            2WalksOnOt     
 
  
    2WalksOnOt        |
83 | 79, 80, 82 | 3bitri 275 |
. . . . 5
   
  
    2WalksOnOt     

  
    2WalksOnOt        |
84 | 75, 83 | syl6bb 265 |
. . . 4
  USGrph

 
   
  
  
        
   2WalksOnOt         |
85 | 14, 16 | syl 17 |
. . . . . 6
  USGrph

 
        2WalksOnOt        
   2WalksOnOt        |
86 | 85 | bicomd 205 |
. . . . 5
  USGrph

 
 
 
     2WalksOnOt
   
  
    2WalksOnOt       |
87 | 86 | anbi2d 710 |
. . . 4
  USGrph

 
  
 
     2WalksOnOt
         
   2WalksOnOt        |
88 | 84, 87 | bitrd 257 |
. . 3
  USGrph

 
   
  
  
       
   2WalksOnOt        |
89 | | simpll 760 |
. . . . . . 7
   USGrph 
   USGrph   |
90 | 7 | adantr 467 |
. . . . . . 7
   USGrph 
   
   |
91 | | simpr 463 |
. . . . . . 7
   USGrph 
     |
92 | 10 | eqcomd 2457 |
. . . . . . 7
  USGrph



  
2WalksOnOt       2SPathOnOt
     |
93 | 89, 90, 91, 92 | syl3anc 1268 |
. . . . . 6
   USGrph 
      2WalksOnOt       2SPathOnOt      |
94 | 93 | eleq2d 2514 |
. . . . 5
   USGrph 
           2WalksOnOt
  
  
    2SPathOnOt       |
95 | 94 | biimpd 211 |
. . . 4
   USGrph 
           2WalksOnOt
     
    2SPathOnOt       |
96 | 95 | expimpd 608 |
. . 3
  USGrph

 
         2WalksOnOt    
  
    2SPathOnOt       |
97 | 88, 96 | sylbid 219 |
. 2
  USGrph

 
   
  
  
      
   2SPathOnOt       |
98 | 58, 97 | impbid 194 |
1
  USGrph

 
        2SPathOnOt            
      |