Step | Hyp | Ref
| Expression |
1 | | df-spth 25318 |
. . 3
SPaths          Trails        |
2 | 1 | brovmpt2ex 6988 |
. 2
   SPaths  
 
 
    |
3 | | simprl 772 |
. . . . 5
   


     Trails        Trails     |
4 | | funres11 5661 |
. . . . . . 7
 
 
 ..^        |
5 | 4 | adantl 473 |
. . . . . 6
    Trails        ..^        |
6 | 5 | adantl 473 |
. . . . 5
   


     Trails         ..^        |
7 | | trliswlk 25348 |
. . . . . . . . . 10
   Trails  
  Walks     |
8 | 7 | a1i 11 |
. . . . . . . . 9
      
   Trails
    Walks      |
9 | | 2mwlk 25328 |
. . . . . . . . 9
   Walks  
 Word                |
10 | 8, 9 | syl6 33 |
. . . . . . . 8
      
   Trails
   Word                 |
11 | 10 | imp 436 |
. . . . . . 7
   


    Trails     Word                |
12 | | imain 5669 |
. . . . . . . . . . 11
 
            ..^                       ..^         |
13 | 12 | adantl 473 |
. . . . . . . . . 10
  Word               ..^                       ..^         |
14 | | 0lt1 10157 |
. . . . . . . . . . . . . . . . . 18
 |
15 | | 0re 9661 |
. . . . . . . . . . . . . . . . . . 19
 |
16 | | 1re 9660 |
. . . . . . . . . . . . . . . . . . 19
 |
17 | 15, 16 | ltnlei 9773 |
. . . . . . . . . . . . . . . . . 18

  |
18 | 14, 17 | mpbi 213 |
. . . . . . . . . . . . . . . . 17
 |
19 | | elfzole1 11955 |
. . . . . . . . . . . . . . . . 17
  ..^    
  |
20 | 18, 19 | mto 181 |
. . . . . . . . . . . . . . . 16
 ..^      |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . 15
 Word
 ..^       |
22 | | wrdfin 12736 |
. . . . . . . . . . . . . . . . . . 19
 Word
  |
23 | | hashcl 12576 |
. . . . . . . . . . . . . . . . . . . 20
       |
24 | 23 | nn0red 10950 |
. . . . . . . . . . . . . . . . . . 19
       |
25 | 22, 24 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 Word
      |
26 | 25 | ltnrd 9786 |
. . . . . . . . . . . . . . . . 17
 Word
   
      |
27 | 26 | intn3an3d 1409 |
. . . . . . . . . . . . . . . 16
 Word
                        |
28 | | elfzo2 11950 |
. . . . . . . . . . . . . . . 16
      ..^    
                        |
29 | 27, 28 | sylnibr 312 |
. . . . . . . . . . . . . . 15
 Word
     ..^       |
30 | | fvex 5889 |
. . . . . . . . . . . . . . . 16
     |
31 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . 18
   ..^    
 ..^        |
32 | 31 | notbid 301 |
. . . . . . . . . . . . . . . . 17
 
 ..^    
 ..^        |
33 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . 18
    
  ..^    
     ..^        |
34 | 33 | notbid 301 |
. . . . . . . . . . . . . . . . 17
    

 ..^    
     ..^        |
35 | 32, 34 | ralprg 4012 |
. . . . . . . . . . . . . . . 16
                 ..^    

 ..^          ..^         |
36 | 15, 30, 35 | mp2an 686 |
. . . . . . . . . . . . . . 15
 
        ..^    

 ..^          ..^        |
37 | 21, 29, 36 | sylanbrc 677 |
. . . . . . . . . . . . . 14
 Word
         ..^       |
38 | | disj 3809 |
. . . . . . . . . . . . . 14
          ..^      
        ..^       |
39 | 37, 38 | sylibr 217 |
. . . . . . . . . . . . 13
 Word
         ..^        |
40 | 39 | imaeq2d 5174 |
. . . . . . . . . . . 12
 Word
            ..^             |
41 | | ima0 5189 |
. . . . . . . . . . . 12
     |
42 | 40, 41 | syl6eq 2521 |
. . . . . . . . . . 11
 Word
            ..^         |
43 | 42 | adantr 472 |
. . . . . . . . . 10
  Word               ..^         |
44 | 13, 43 | eqtr3d 2507 |
. . . . . . . . 9
  Word                   ..^         |
45 | 44 | ex 441 |
. . . . . . . 8
 Word
                  ..^          |
46 | 45 | adantr 472 |
. . . . . . 7
  Word                                ..^          |
47 | 11, 46 | syl 17 |
. . . . . 6
   


    Trails    
                 ..^          |
48 | 47 | impr 631 |
. . . . 5
   


     Trails                      ..^         |
49 | 3, 6, 48 | 3jca 1210 |
. . . 4
   


     Trails         Trails      ..^                      ..^          |
50 | 49 | ex 441 |
. . 3
      
    Trails        Trails      ..^                      ..^           |
51 | | isspth 25378 |
. . 3
      
   SPaths
     Trails        |
52 | | ispth 25377 |
. . 3
      
   Paths
     Trails      ..^                      ..^           |
53 | 50, 51, 52 | 3imtr4d 276 |
. 2
      
   SPaths
    Paths      |
54 | 2, 53 | mpcom 36 |
1
   SPaths  
  Paths     |