Step | Hyp | Ref
| Expression |
1 | | 1trl.f |
. . 3
      |
2 | | c0ex 9634 |
. . . . . . 7
 |
3 | | vex 3047 |
. . . . . . 7
 |
4 | 2, 3 | f1osn 5850 |
. . . . . 6
  
           |
5 | | f1of1 5811 |
. . . . . 6
                             |
6 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
                     |
7 | | opex 4663 |
. . . . . . . . . . . . . . . . 17
    |
8 | | hashsng 12546 |
. . . . . . . . . . . . . . . . 17
   
           |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
          |
10 | 6, 9 | syl6eq 2500 |
. . . . . . . . . . . . . . 15
            |
11 | 1, 10 | ax-mp 5 |
. . . . . . . . . . . . . 14
     |
12 | 11 | oveq2i 6299 |
. . . . . . . . . . . . 13
 ..^      ..^  |
13 | | fzo01 11992 |
. . . . . . . . . . . . 13
 ..^    |
14 | 12, 13 | eqtri 2472 |
. . . . . . . . . . . 12
 ..^        |
15 | 14 | eqcomi 2459 |
. . . . . . . . . . 11
   ..^      |
16 | | f1eq2 5773 |
. . . . . . . . . . 11
    ..^                  
        ..^            |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . 10
             
        ..^           |
18 | 17 | biimpi 198 |
. . . . . . . . 9
                      ..^           |
19 | 18 | adantr 467 |
. . . . . . . 8
                  
                  ..^           |
20 | | prid1g 4077 |
. . . . . . . . . . . . . 14
      |
21 | 20 | adantr 467 |
. . . . . . . . . . . . 13
 
      |
22 | 21 | 3ad2ant2 1029 |
. . . . . . . . . . . 12
  


              |
23 | 22 | adantl 468 |
. . . . . . . . . . 11
                  
           
   |
24 | | eleq2 2517 |
. . . . . . . . . . . . 13
       
    
      |
25 | 24 | 3ad2ant3 1030 |
. . . . . . . . . . . 12
  


         
   
      |
26 | 25 | adantl 468 |
. . . . . . . . . . 11
                  
              
      |
27 | 23, 26 | mpbird 236 |
. . . . . . . . . 10
                  
                |
28 | | elfvdm 5889 |
. . . . . . . . . 10
       |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
                  
            |
30 | 29 | snssd 4116 |
. . . . . . . 8
                  
           
  |
31 | | f1ss 5782 |
. . . . . . . 8
          ..^          
         ..^         |
32 | 19, 30, 31 | syl2anc 666 |
. . . . . . 7
                  
                  ..^         |
33 | 32 | ex 436 |
. . . . . 6
                  
                 ..^          |
34 | 4, 5, 33 | mp2b 10 |
. . . . 5
  


           
     ..^         |
35 | 34 | adantl 468 |
. . . 4
    
     
                  ..^         |
36 | | f1eq1 5772 |
. . . . 5
          ..^               ..^          |
37 | 36 | adantr 467 |
. . . 4
    
     
              ..^               ..^          |
38 | 35, 37 | mpbird 236 |
. . 3
    
     
             ..^         |
39 | 1, 38 | mpan 675 |
. 2
  


            ..^         |
40 | | 1trl.p |
. . . 4
          |
41 | | 0z 10945 |
. . . . . . . . 9
 |
42 | | 1z 10964 |
. . . . . . . . 9
 |
43 | 41, 42 | pm3.2i 457 |
. . . . . . . 8
   |
44 | | 0ne1 10674 |
. . . . . . . 8
 |
45 | | fprg 6071 |
. . . . . . . . 9
         
                  |
46 | | 0p1e1 10718 |
. . . . . . . . . . . . 13
   |
47 | 46 | eqcomi 2459 |
. . . . . . . . . . . 12
   |
48 | 47 | oveq2i 6299 |
. . . . . . . . . . 11
           |
49 | | fzpr 11848 |
. . . . . . . . . . . 12
              |
50 | 41, 49 | ax-mp 5 |
. . . . . . . . . . 11
            |
51 | 46 | preq2i 4054 |
. . . . . . . . . . 11
         |
52 | 48, 50, 51 | 3eqtri 2476 |
. . . . . . . . . 10
        |
53 | 52 | feq2i 5719 |
. . . . . . . . 9
                                          |
54 | 45, 53 | sylibr 216 |
. . . . . . . 8
         
                   |
55 | 43, 44, 54 | mp3an13 1354 |
. . . . . . 7
 
                       |
56 | | prssi 4127 |
. . . . . . 7
 
      |
57 | 55, 56 | fssd 5736 |
. . . . . 6
 
                    |
58 | 57 | adantl 468 |
. . . . 5
    
                            |
59 | | id 22 |
. . . . . . 7
                     |
60 | 11 | oveq2i 6299 |
. . . . . . . 8
             |
61 | 60 | a1i 11 |
. . . . . . 7
                        |
62 | 59, 61 | feq12d 5715 |
. . . . . 6
                      
                    |
63 | 62 | adantr 467 |
. . . . 5
    
                                          |
64 | 58, 63 | mpbird 236 |
. . . 4
    
                       |
65 | 40, 64 | mpan 675 |
. . 3
 
               |
66 | 65 | 3ad2ant2 1029 |
. 2
  


                       |
67 | | id 22 |
. . . . . 6
       
         |
68 | 67 | 3ad2ant3 1030 |
. . . . 5
  


                  |
69 | | fveq1 5862 |
. . . . . . . . 9
             
       |
70 | 2, 3 | fvsn 6095 |
. . . . . . . . 9
          |
71 | 69, 70 | syl6eq 2500 |
. . . . . . . 8
            |
72 | 1, 71 | ax-mp 5 |
. . . . . . 7
     |
73 | 72 | a1i 11 |
. . . . . 6
  


               |
74 | 73 | fveq2d 5867 |
. . . . 5
  


                       |
75 | | fveq1 5862 |
. . . . . . . . . 10
                 
           |
76 | | fvpr1g 6107 |
. . . . . . . . . . 11
 
                |
77 | 2, 44, 76 | mp3an13 1354 |
. . . . . . . . . 10
                |
78 | 75, 77 | sylan9eq 2504 |
. . . . . . . . 9
    
             |
79 | 40, 78 | mpan 675 |
. . . . . . . 8
       |
80 | 79 | adantr 467 |
. . . . . . 7
 
       |
81 | 80 | 3ad2ant2 1029 |
. . . . . 6
  


               |
82 | | fveq1 5862 |
. . . . . . . . . 10
                 
           |
83 | | 1ex 9635 |
. . . . . . . . . . 11
 |
84 | | fvpr2g 6108 |
. . . . . . . . . . 11
 
                |
85 | 83, 44, 84 | mp3an13 1354 |
. . . . . . . . . 10
                |
86 | 82, 85 | sylan9eq 2504 |
. . . . . . . . 9
    
             |
87 | 40, 86 | mpan 675 |
. . . . . . . 8
       |
88 | 87 | adantl 468 |
. . . . . . 7
 
       |
89 | 88 | 3ad2ant2 1029 |
. . . . . 6
  


               |
90 | 81, 89 | preq12d 4058 |
. . . . 5
  


                         |
91 | 68, 74, 90 | 3eqtr4d 2494 |
. . . 4
  


                              |
92 | | fveq2 5863 |
. . . . . . 7
           |
93 | 92 | fveq2d 5867 |
. . . . . 6
                   |
94 | | fveq2 5863 |
. . . . . . 7
           |
95 | | oveq1 6295 |
. . . . . . . . 9
       |
96 | 95, 46 | syl6eq 2500 |
. . . . . . . 8
     |
97 | 96 | fveq2d 5867 |
. . . . . . 7
             |
98 | 94, 97 | preq12d 4058 |
. . . . . 6
                           |
99 | 93, 98 | eqeq12d 2465 |
. . . . 5
                      
                      |
100 | 2, 99 | ralsn 4009 |
. . . 4
 
                      
                     |
101 | 91, 100 | sylibr 216 |
. . 3
  


                                   |
102 | 14 | a1i 11 |
. . . 4
  


          ..^         |
103 | 102 | raleqdv 2992 |
. . 3
  


          
 ..^                                                      |
104 | 101, 103 | mpbird 236 |
. 2
  


           ..^                             |
105 | | snex 4640 |
. . . . 5
  
   |
106 | 1, 105 | eqeltri 2524 |
. . . 4
 |
107 | | prex 4641 |
. . . . 5
  
       |
108 | 40, 107 | eqeltri 2524 |
. . . 4
 |
109 | | istrl2 25261 |
. . . 4
  

      Trails  
    ..^                     ..^                               |
110 | 106, 108,
109 | mpanr12 690 |
. . 3
 
    Trails  
    ..^                     ..^                               |
111 | 110 | 3ad2ant1 1028 |
. 2
  


            Trails  
    ..^                     ..^                               |
112 | 39, 66, 104, 111 | mpbir3and 1190 |
1
  


           Trails
    |