Step | Hyp | Ref
| Expression |
1 | | pthistrl 25302 |
. . . . . 6
   Paths  
  Trails     |
2 | | trliswlk 25269 |
. . . . . 6
   Trails  
  Walks     |
3 | | wlkbprop 25251 |
. . . . . 6
   Walks  
    
  
    |
4 | 1, 2, 3 | 3syl 18 |
. . . . 5
   Paths  
    
  
    |
5 | | ispth 25298 |
. . . . . . 7
      
   Paths
     Trails      ..^                      ..^           |
6 | 5 | 3adant1 1026 |
. . . . . 6
      
   
   Paths
     Trails      ..^                      ..^           |
7 | | 3anass 989 |
. . . . . . . . . . 11
    Trails      ..^                      ..^       
   Trails     
 ..^                      ..^           |
8 | | istrl2 25268 |
. . . . . . . . . . . . . . . 16
      
   Trails
      ..^                     ..^                               |
9 | 8 | 3adant1 1026 |
. . . . . . . . . . . . . . 15
      
   
   Trails
      ..^                     ..^                               |
10 | 9 | adantr 467 |
. . . . . . . . . . . . . 14
       
   
USGrph     Trails       ..^                     ..^                               |
11 | 10 | adantr 467 |
. . . . . . . . . . . . 13
            
USGrph          Trails       ..^                     ..^                               |
12 | | fzo0to2pr 11998 |
. . . . . . . . . . . . . . . . . . . 20
 ..^     |
13 | 12 | raleqi 2991 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^                                            
     |
14 | | 2wlklem 25294 |
. . . . . . . . . . . . . . . . . . 19
 
                                                                  |
15 | 13, 14 | bitri 253 |
. . . . . . . . . . . . . . . . . 18
 
 ..^                                                                 |
16 | | usgraf1 25087 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 USGrph       |
17 | 16 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
   
USGrph        |
18 | 17 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ..^                  
   
USGrph  
      |
19 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ..^                  
   
USGrph  
   ..^     |
20 | | 2nn 10767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
21 | | lbfzo0 11955 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  ..^   |
22 | 20, 21 | mpbir 213 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 ..^  |
23 | | 1ex 9638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
24 | 23 | prid2 4081 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    |
25 | 24, 12 | eleqtrri 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 ..^  |
26 | 22, 25 | pm3.2i 457 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ..^  ..^   |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ..^                  
   
USGrph  
  ..^  ..^    |
28 | | 0ne1 10677 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ..^                  
   
USGrph  
  |
30 | | 2f1fvneq 39014 |
. . . . . . . . . . . . . . . . . . . . . . 23
          ..^      ..^
 ..^                                                                     |
31 | 18, 19, 27, 29, 30 | syl211anc 1274 |
. . . . . . . . . . . . . . . . . . . . . 22
      ..^                  
   
USGrph  
                                                                  |
32 | 31 | impancom 442 |
. . . . . . . . . . . . . . . . . . . . 21
      ..^                                                            
   
USGrph                           |
33 | 32 | imp 431 |
. . . . . . . . . . . . . . . . . . . 20
       ..^                                                               
USGrph  
                        |
34 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       ..^                                                               
USGrph  
          |
35 | 34 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                              ..^                                                               
USGrph              |
36 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
37 | | usgranloopv 25105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  USGrph
                                    |
38 | 36, 37 | mpan2 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 USGrph                    
           |
39 | 38 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                     USGrph
           |
40 | 39 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                          USGrph
           |
41 | 40 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  USGrph
                                                   |
42 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
43 | | usgranloopv 25105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  USGrph
                                    |
44 | 42, 43 | mpan2 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 USGrph                    
           |
45 | 44 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                     USGrph
           |
46 | 45 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                          USGrph
           |
47 | 46 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  USGrph
                                                   |
48 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
49 | 36, 42, 48 | 3pm3.2i 1186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
               |
50 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                             |
51 | | pr1nebg 38992 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                                           |
52 | 49, 50, 51 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                                     |
53 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                            
          |
54 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                            
          |
55 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                            
          |
56 | 53, 54, 55 | 3jca 1188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                            
        
       
           |
57 | 56 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                                         |
58 | 52, 57 | sylbird 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                                  
       
            |
59 | 41, 47, 58 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  USGrph
                                                                        
       
            |
60 | 59 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 USGrph                                                                         
       
             |
61 | 60 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
   
USGrph                                                                          
       
             |
62 | 61 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                                  
  USGrph                                                       |
63 | 62 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      ..^                                                            
   
USGrph                                 
       
             |
64 | 63 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       ..^                                                               
USGrph  
                                                    |
65 | 64 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                              ..^                                                               
USGrph                                |
66 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
67 | 66 | f13idfv 12212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
                                      |
68 | 35, 65, 67 | sylanbrc 670 |
. . . . . . . . . . . . . . . . . . . . . . 23
                              ..^                                                               
USGrph              |
69 | | df-f1 5587 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
             |
70 | 68, 69 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . 22
                              ..^                                                               
USGrph                 |
71 | 70 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . 21
                              ..^                                                               
USGrph       |
72 | 71 | a1d 26 |
. . . . . . . . . . . . . . . . . . . 20
                              ..^                                                               
USGrph     
   ..^              ..^   
    |
73 | 33, 72 | mpancom 675 |
. . . . . . . . . . . . . . . . . . 19
       ..^                                                               
USGrph  
     ..^              ..^        |
74 | 73 | exp31 609 |
. . . . . . . . . . . . . . . . . 18
     ..^           
                                                  
  USGrph   
   ..^              ..^   
      |
75 | 15, 74 | syl5bi 221 |
. . . . . . . . . . . . . . . . 17
     ..^           
 
 ..^                      
       
   
USGrph       ..^              ..^          |
76 | 75 | 3impia 1205 |
. . . . . . . . . . . . . . . 16
     ..^             ..^                   
           
   
USGrph       ..^              ..^         |
77 | 76 | com12 32 |
. . . . . . . . . . . . . . 15
       
   
USGrph       ..^             ..^                         
   ..^              ..^   
     |
78 | 77 | adantr 467 |
. . . . . . . . . . . . . 14
            
USGrph            ..^             ..^                         
   ..^              ..^   
     |
79 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . 18
       |
80 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . 18
      ..^      ..^   |
81 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . 18
       |
82 | 79, 80, 81 | f1eq123d 5809 |
. . . . . . . . . . . . . . . . 17
         ..^      
   ..^      |
83 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . 18
                   |
84 | 83 | feq2d 5715 |
. . . . . . . . . . . . . . . . 17
                 
           |
85 | 80 | raleqdv 2993 |
. . . . . . . . . . . . . . . . 17
      
 ..^                             ..^                          |
86 | 82, 84, 85 | 3anbi123d 1339 |
. . . . . . . . . . . . . . . 16
          ..^                     ..^                           
    ..^             ..^                           |
87 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . 21
      ..^      ..^   |
88 | 87 | reseq2d 5105 |
. . . . . . . . . . . . . . . . . . . 20
       ..^      
 ..^    |
89 | 88 | cnveqd 5010 |
. . . . . . . . . . . . . . . . . . 19
      
 ..^         ..^    |
90 | 89 | funeqd 5603 |
. . . . . . . . . . . . . . . . . 18
         ..^     
 
 ..^     |
91 | | preq2 4052 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
92 | 91 | imaeq2d 5168 |
. . . . . . . . . . . . . . . . . . . 20
                         |
93 | 87 | imaeq2d 5168 |
. . . . . . . . . . . . . . . . . . . 20
         ..^          ..^    |
94 | 92, 93 | ineq12d 3635 |
. . . . . . . . . . . . . . . . . . 19
                     ..^                   ..^     |
95 | 94 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . . 18
                      ..^                   ..^      |
96 | 90, 95 | anbi12d 717 |
. . . . . . . . . . . . . . . . 17
      
   ..^                      ..^       
    ..^              ..^       |
97 | 96 | imbi1d 319 |
. . . . . . . . . . . . . . . 16
         
 ..^                      ..^       
 
     ..^              ..^         |
98 | 86, 97 | imbi12d 322 |
. . . . . . . . . . . . . . 15
           ..^                     ..^                               
 ..^                      ..^       
  
     ..^             ..^                         
   ..^              ..^   
      |
99 | 98 | adantl 468 |
. . . . . . . . . . . . . 14
            
USGrph             ..^                     ..^                             
   ..^                      ..^          
     ..^             ..^                         
   ..^              ..^   
      |
100 | 78, 99 | mpbird 236 |
. . . . . . . . . . . . 13
            
USGrph            ..^                     ..^                             
   ..^                      ..^             |
101 | 11, 100 | sylbid 219 |
. . . . . . . . . . . 12
            
USGrph          Trails        ..^                      ..^       
     |
102 | 101 | imdistand 698 |
. . . . . . . . . . 11
            
USGrph           Trails       ..^                      ..^            Trails        |
103 | 7, 102 | syl5bi 221 |
. . . . . . . . . 10
            
USGrph           Trails    
 ..^                      ..^       
   Trails        |
104 | 103 | imp 431 |
. . . . . . . . 9
           
  USGrph          Trails      ..^                      ..^            Trails       |
105 | | isspth 25299 |
. . . . . . . . . . 11
      
   SPaths
     Trails        |
106 | 105 | 3adant1 1026 |
. . . . . . . . . 10
      
   
   SPaths
     Trails        |
107 | 106 | ad3antrrr 736 |
. . . . . . . . 9
           
  USGrph          Trails      ..^                      ..^            SPaths  
   Trails
       |
108 | 104, 107 | mpbird 236 |
. . . . . . . 8
           
  USGrph          Trails      ..^                      ..^           SPaths
    |
109 | 108 | exp41 615 |
. . . . . . 7
      
   
 USGrph          Trails    
 ..^                      ..^       
  SPaths        |
110 | 109 | com24 90 |
. . . . . 6
      
   
    Trails      ..^                      ..^       
      USGrph
  SPaths        |
111 | 6, 110 | sylbid 219 |
. . . . 5
      
   
   Paths
        USGrph   SPaths        |
112 | 4, 111 | mpcom 37 |
. . . 4
   Paths  
    
 USGrph   SPaths       |
113 | 112 | com13 83 |
. . 3
 USGrph         Paths     SPaths       |
114 | 113 | imp 431 |
. 2
  USGrph
        Paths     SPaths
     |
115 | | spthispth 25303 |
. 2
   SPaths  
  Paths     |
116 | 114, 115 | impbid1 207 |
1
  USGrph
        Paths  
  SPaths      |