Step | Hyp | Ref
| Expression |
1 | | mbfpos.1 |
. . 3
 
   |
2 | | eqid 2453 |
. . 3
     |
3 | 1, 2 | fmptd 6051 |
. 2
         |
4 | | mbfposr.2 |
. . 3
    
   MblFn |
5 | | 0re 9648 |
. . . 4
 |
6 | | ifcl 3925 |
. . . 4
 
   
    |
7 | 1, 5, 6 | sylancl 669 |
. . 3
 
        |
8 | 4, 7 | mbfdm2 22606 |
. 2
   |
9 | | simplr 763 |
. . . . . . . . . . . . . 14
   


   |
10 | | simpllr 770 |
. . . . . . . . . . . . . . 15
   


   |
11 | 10 | lt0neg1d 10190 |
. . . . . . . . . . . . . 14
   


 
    |
12 | 9, 11 | mpbid 214 |
. . . . . . . . . . . . 13
   


    |
13 | 12 | biantrurd 511 |
. . . . . . . . . . . 12
   


            |
14 | | simpll 761 |
. . . . . . . . . . . . . 14
       |
15 | 14, 1 | sylan 474 |
. . . . . . . . . . . . 13
   


   |
16 | 10, 15 | ltnegd 10198 |
. . . . . . . . . . . 12
   


 
     |
17 | | 0red 9649 |
. . . . . . . . . . . . 13
   


   |
18 | 15 | renegcld 10053 |
. . . . . . . . . . . . 13
   


    |
19 | 10 | renegcld 10053 |
. . . . . . . . . . . . 13
   


    |
20 | | maxlt 11494 |
. . . . . . . . . . . . 13
       
     
        |
21 | 17, 18, 19, 20 | syl3anc 1269 |
. . . . . . . . . . . 12
   


                  |
22 | 13, 16, 21 | 3bitr4rd 290 |
. . . . . . . . . . 11
   


             |
23 | 1 | renegcld 10053 |
. . . . . . . . . . . . . 14
 
    |
24 | | ifcl 3925 |
. . . . . . . . . . . . . 14
         
   |
25 | 23, 5, 24 | sylancl 669 |
. . . . . . . . . . . . 13
 
          |
26 | 14, 25 | sylan 474 |
. . . . . . . . . . . 12
   


          |
27 | 26 | biantrurd 511 |
. . . . . . . . . . 11
   


                   
          |
28 | 15 | biantrurd 511 |
. . . . . . . . . . 11
   


 
     |
29 | 22, 27, 28 | 3bitr3d 287 |
. . . . . . . . . 10
   


        
               |
30 | 19 | rexrd 9695 |
. . . . . . . . . . 11
   


    |
31 | | elioomnf 11736 |
. . . . . . . . . . 11
 
           
                    |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
   


            
                    |
33 | 10 | rexrd 9695 |
. . . . . . . . . . 11
   


   |
34 | | elioopnf 11735 |
. . . . . . . . . . 11

   
     |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
   


 
  
     |
36 | 29, 32, 35 | 3bitr4d 289 |
. . . . . . . . 9
   


            
      |
37 | | simpr 463 |
. . . . . . . . . . . 12
 
   |
38 | | eqid 2453 |
. . . . . . . . . . . . 13
  
        
       |
39 | 38 | fvmpt2 5962 |
. . . . . . . . . . . 12
             
              
   |
40 | 37, 25, 39 | syl2anc 667 |
. . . . . . . . . . 11
 
                       |
41 | 40 | eleq1d 2515 |
. . . . . . . . . 10
 
         
        
 
            |
42 | 14, 41 | sylan 474 |
. . . . . . . . 9
   


         
        
 
            |
43 | 2 | fvmpt2 5962 |
. . . . . . . . . . . 12
 
         |
44 | 37, 1, 43 | syl2anc 667 |
. . . . . . . . . . 11
 
         |
45 | 44 | eleq1d 2515 |
. . . . . . . . . 10
 
                 |
46 | 14, 45 | sylan 474 |
. . . . . . . . 9
   


                 |
47 | 36, 42, 46 | 3bitr4d 289 |
. . . . . . . 8
   


         
        
            |
48 | 47 | pm5.32da 647 |
. . . . . . 7
              
         

             |
49 | 25, 38 | fmptd 6051 |
. . . . . . . . 9
                |
50 | | ffn 5733 |
. . . . . . . . 9
                    
    |
51 | | elpreima 6007 |
. . . . . . . . 9
                   
                 
             |
52 | 49, 50, 51 | 3syl 18 |
. . . . . . . 8
          
                 
             |
53 | 52 | ad2antrr 733 |
. . . . . . 7
                       

                     |
54 | | ffn 5733 |
. . . . . . . . 9
           |
55 | | elpreima 6007 |
. . . . . . . . 9
             

             |
56 | 3, 54, 55 | 3syl 18 |
. . . . . . . 8
           

             |
57 | 56 | ad2antrr 733 |
. . . . . . 7
             
                |
58 | 48, 53, 57 | 3bitr4d 289 |
. . . . . 6
                       
             |
59 | 58 | alrimiv 1775 |
. . . . 5
                
                
     |
60 | | nfmpt1 4495 |
. . . . . . . 8
            |
61 | 60 | nfcnv 5016 |
. . . . . . 7
         
   |
62 | | nfcv 2594 |
. . . . . . 7
       |
63 | 61, 62 | nfima 5179 |
. . . . . 6
      
              |
64 | | nfmpt1 4495 |
. . . . . . . 8
     |
65 | 64 | nfcnv 5016 |
. . . . . . 7
      |
66 | | nfcv 2594 |
. . . . . . 7
      |
67 | 65, 66 | nfima 5179 |
. . . . . 6
             |
68 | 63, 67 | cleqf 2619 |
. . . . 5
         
                          
                    
     |
69 | 59, 68 | sylibr 216 |
. . . 4
             
                     |
70 | | mbfposr.3 |
. . . . . 6
          MblFn |
71 | | mbfima 22600 |
. . . . . 6
           MblFn

 
                               |
72 | 70, 49, 71 | syl2anc 667 |
. . . . 5
     
               |
73 | 72 | ad2antrr 733 |
. . . 4
             
           |
74 | 69, 73 | eqeltrrd 2532 |
. . 3
                 |
75 | | 0red 9649 |
. . . . . . . . . . . . . . 15
   

 
  |
76 | | simpll 761 |
. . . . . . . . . . . . . . . 16
       |
77 | 76, 1 | sylan 474 |
. . . . . . . . . . . . . . 15
   

 
  |
78 | | simpllr 770 |
. . . . . . . . . . . . . . 15
   

 
  |
79 | | maxle 11492 |
. . . . . . . . . . . . . . 15
 
      
     |
80 | 75, 77, 78, 79 | syl3anc 1269 |
. . . . . . . . . . . . . 14
   

 
     
     |
81 | | simplr 763 |
. . . . . . . . . . . . . . 15
   

 
  |
82 | 81 | biantrurd 511 |
. . . . . . . . . . . . . 14
   

 
 
    |
83 | 80, 82 | bitr4d 260 |
. . . . . . . . . . . . 13
   

 
     
   |
84 | 83 | notbid 296 |
. . . . . . . . . . . 12
   

 
     
   |
85 | 77, 5, 6 | sylancl 669 |
. . . . . . . . . . . . 13
   

 
 
 
   |
86 | 78, 85 | ltnled 9787 |
. . . . . . . . . . . 12
   

 
   
 
        |
87 | 78, 77 | ltnled 9787 |
. . . . . . . . . . . 12
   

 

   |
88 | 84, 86, 87 | 3bitr4d 289 |
. . . . . . . . . . 11
   

 
   
 
   |
89 | 85 | biantrurd 511 |
. . . . . . . . . . 11
   

 
   
 
        
      |
90 | 77 | biantrurd 511 |
. . . . . . . . . . 11
   

 
      |
91 | 88, 89, 90 | 3bitr3d 287 |
. . . . . . . . . 10
   

 
         
  
     |
92 | 78 | rexrd 9695 |
. . . . . . . . . . 11
   

 
  |
93 | | elioopnf 11735 |
. . . . . . . . . . 11

        
  
 
   
      |
94 | 92, 93 | syl 17 |
. . . . . . . . . 10
   

 
        
  
 
   
      |
95 | 92, 34 | syl 17 |
. . . . . . . . . 10
   

 
         |
96 | 91, 94, 95 | 3bitr4d 289 |
. . . . . . . . 9
   

 
        
 
    |
97 | | eqid 2453 |
. . . . . . . . . . . . 13
  
 
    
 
   |
98 | 97 | fvmpt2 5962 |
. . . . . . . . . . . 12
                     
    |
99 | 37, 7, 98 | syl2anc 667 |
. . . . . . . . . . 11
 
     
             |
100 | 99 | eleq1d 2515 |
. . . . . . . . . 10
 
                  
        |
101 | 76, 100 | sylan 474 |
. . . . . . . . 9
   

 
     
                    |
102 | 76, 45 | sylan 474 |
. . . . . . . . 9
   

 
         
      |
103 | 96, 101, 102 | 3bitr4d 289 |
. . . . . . . 8
   

 
     
                     |
104 | 103 | pm5.32da 647 |
. . . . . . 7
                     

             |
105 | 7, 97 | fmptd 6051 |
. . . . . . . . 9
    
         |
106 | | ffn 5733 |
. . . . . . . . 9
                     |
107 | | elpreima 6007 |
. . . . . . . . 9
                       

    
             |
108 | 105, 106,
107 | 3syl 18 |
. . . . . . . 8
                

    
             |
109 | 108 | ad2antrr 733 |
. . . . . . 7
           
        

    
             |
110 | 56 | ad2antrr 733 |
. . . . . . 7
             
                |
111 | 104, 109,
110 | 3bitr4d 289 |
. . . . . 6
           
        
             |
112 | 111 | alrimiv 1775 |
. . . . 5
                      
             |
113 | | nfmpt1 4495 |
. . . . . . . 8
     
    |
114 | 113 | nfcnv 5016 |
. . . . . . 7
           |
115 | 114, 66 | nfima 5179 |
. . . . . 6
      
 
         |
116 | 115, 67 | cleqf 2619 |
. . . . 5
                         
                 
             |
117 | 112, 116 | sylibr 216 |
. . . 4
                                |
118 | | mbfima 22600 |
. . . . . 6
     
   MblFn    
            
 
          |
119 | 4, 105, 118 | syl2anc 667 |
. . . . 5
     
 
          |
120 | 119 | ad2antrr 733 |
. . . 4
                      |
121 | 117, 120 | eqeltrrd 2532 |
. . 3
                 |
122 | | simpr 463 |
. . 3
 

  |
123 | | 0red 9649 |
. . 3
 

  |
124 | 74, 121, 122, 123 | ltlecasei 9747 |
. 2
 

       
    |
125 | | 0red 9649 |
. . . . . . . . . . . . 13
   

 
  |
126 | | simpll 761 |
. . . . . . . . . . . . . 14
       |
127 | 126, 1 | sylan 474 |
. . . . . . . . . . . . 13
   

 
  |
128 | | simpllr 770 |
. . . . . . . . . . . . 13
   

 
  |
129 | | maxlt 11494 |
. . . . . . . . . . . . 13
 
      
     |
130 | 125, 127,
128, 129 | syl3anc 1269 |
. . . . . . . . . . . 12
   

 
     
     |
131 | | simplr 763 |
. . . . . . . . . . . . 13
   

 
  |
132 | 131 | biantrurd 511 |
. . . . . . . . . . . 12
   

 
 
    |
133 | 130, 132 | bitr4d 260 |
. . . . . . . . . . 11
   

 
     
   |
134 | 126, 7 | sylan 474 |
. . . . . . . . . . . 12
   

 
 
 
   |
135 | 134 | biantrurd 511 |
. . . . . . . . . . 11
   

 
     
               |
136 | 127 | biantrurd 511 |
. . . . . . . . . . 11
   

 
      |
137 | 133, 135,
136 | 3bitr3d 287 |
. . . . . . . . . 10
   

 
            
     |
138 | 128 | rexrd 9695 |
. . . . . . . . . . 11
   

 
  |
139 | | elioomnf 11736 |
. . . . . . . . . . 11

        
               |
140 | 138, 139 | syl 17 |
. . . . . . . . . 10
   

 
        
               |
141 | | elioomnf 11736 |
. . . . . . . . . . 11

   
     |
142 | 138, 141 | syl 17 |
. . . . . . . . . 10
   

 

        |
143 | 137, 140,
142 | 3bitr4d 289 |
. . . . . . . . 9
   

 
        
      |
144 | 99 | eleq1d 2515 |
. . . . . . . . . 10
 
                  
        |
145 | 126, 144 | sylan 474 |
. . . . . . . . 9
   

 
     
           
        |
146 | 44 | eleq1d 2515 |
. . . . . . . . . 10
 
                 |
147 | 126, 146 | sylan 474 |
. . . . . . . . 9
   

 
         
      |
148 | 143, 145,
147 | 3bitr4d 289 |
. . . . . . . 8
   

 
     
                     |
149 | 148 | pm5.32da 647 |
. . . . . . 7
                     

             |
150 | | elpreima 6007 |
. . . . . . . . 9
                       

    
             |
151 | 105, 106,
150 | 3syl 18 |
. . . . . . . 8
                

    
             |
152 | 151 | ad2antrr 733 |
. . . . . . 7
           
                            |
153 | | elpreima 6007 |
. . . . . . . . 9
                            |
154 | 3, 54, 153 | 3syl 18 |
. . . . . . . 8
                          |
155 | 154 | ad2antrr 733 |
. . . . . . 7
                              |
156 | 149, 152,
155 | 3bitr4d 289 |
. . . . . 6
           
        
             |
157 | 156 | alrimiv 1775 |
. . . . 5
                      
             |
158 | | nfcv 2594 |
. . . . . . 7
      |
159 | 114, 158 | nfima 5179 |
. . . . . 6
      
 
         |
160 | 65, 158 | nfima 5179 |
. . . . . 6
             |
161 | 159, 160 | cleqf 2619 |
. . . . 5
                         
                 
             |
162 | 157, 161 | sylibr 216 |
. . . 4
                                |
163 | | mbfima 22600 |
. . . . . 6
     
   MblFn    
            
 
          |
164 | 4, 105, 163 | syl2anc 667 |
. . . . 5
     
 
          |
165 | 164 | ad2antrr 733 |
. . . 4
                      |
166 | 162, 165 | eqeltrrd 2532 |
. . 3
                 |
167 | | simplr 763 |
. . . . . . . . . . . . . . . 16
   

 
  |
168 | | simpllr 770 |
. . . . . . . . . . . . . . . . 17
   

 
  |
169 | 168 | le0neg1d 10192 |
. . . . . . . . . . . . . . . 16
   

 
     |
170 | 167, 169 | mpbid 214 |
. . . . . . . . . . . . . . 15
   

 
   |
171 | 170 | biantrurd 511 |
. . . . . . . . . . . . . 14
   

 
  
        |
172 | | simpll 761 |
. . . . . . . . . . . . . . . 16
       |
173 | 172, 1 | sylan 474 |
. . . . . . . . . . . . . . 15
   

 
  |
174 | 168, 173 | lenegd 10199 |
. . . . . . . . . . . . . 14
   

 
      |
175 | | 0red 9649 |
. . . . . . . . . . . . . . 15
   

 
  |
176 | 173 | renegcld 10053 |
. . . . . . . . . . . . . . 15
   

 
   |
177 | 168 | renegcld 10053 |
. . . . . . . . . . . . . . 15
   

 
   |
178 | | maxle 11492 |
. . . . . . . . . . . . . . 15
       
     
        |
179 | 175, 176,
177, 178 | syl3anc 1269 |
. . . . . . . . . . . . . 14
   

 
       

        |
180 | 171, 174,
179 | 3bitr4rd 290 |
. . . . . . . . . . . . 13
   

 
       

   |
181 | 180 | notbid 296 |
. . . . . . . . . . . 12
   

 
       

   |
182 | 172, 25 | sylan 474 |
. . . . . . . . . . . . 13
   

 
 
       |
183 | 177, 182 | ltnled 9787 |
. . . . . . . . . . . 12
   

 
        
      
    |
184 | 173, 168 | ltnled 9787 |
. . . . . . . . . . . 12
   

 

   |
185 | 181, 183,
184 | 3bitr4d 289 |
. . . . . . . . . . 11
   

 
        
   |
186 | 182 | biantrurd 511 |
. . . . . . . . . . 11
   

 
        
          
         |
187 | 173 | biantrurd 511 |
. . . . . . . . . . 11
   

 
      |
188 | 185, 186,
187 | 3bitr3d 287 |
. . . . . . . . . 10
   

 
           
           |
189 | 177 | rexrd 9695 |
. . . . . . . . . . 11
   

 
   |
190 | | elioopnf 11735 |
. . . . . . . . . . 11
 
           
          
         |
191 | 189, 190 | syl 17 |
. . . . . . . . . 10
   

 
           
          
         |
192 | 168 | rexrd 9695 |
. . . . . . . . . . 11
   

 
  |
193 | 192, 141 | syl 17 |
. . . . . . . . . 10
   

 

        |
194 | 188, 191,
193 | 3bitr4d 289 |
. . . . . . . . 9
   

 
           
      |
195 | 40 | eleq1d 2515 |
. . . . . . . . . 10
 
         
        
 
            |
196 | 172, 195 | sylan 474 |
. . . . . . . . 9
   

 
                 
              |
197 | 172, 146 | sylan 474 |
. . . . . . . . 9
   

 
         
      |
198 | 194, 196,
197 | 3bitr4d 289 |
. . . . . . . 8
   

 
                 
            |
199 | 198 | pm5.32da 647 |
. . . . . . 7
              
         

             |
200 | | elpreima 6007 |
. . . . . . . . 9
                   
                 
             |
201 | 49, 50, 200 | 3syl 18 |
. . . . . . . 8
          
                 
             |
202 | 201 | ad2antrr 733 |
. . . . . . 7
                       

                     |
203 | 154 | ad2antrr 733 |
. . . . . . 7
                              |
204 | 199, 202,
203 | 3bitr4d 289 |
. . . . . 6
                       
             |
205 | 204 | alrimiv 1775 |
. . . . 5
                
                      |
206 | | nfcv 2594 |
. . . . . . 7
       |
207 | 61, 206 | nfima 5179 |
. . . . . 6
      
              |
208 | 207, 160 | cleqf 2619 |
. . . . 5
         
                  
           
                      |
209 | 205, 208 | sylibr 216 |
. . . 4
             
                     |
210 | | mbfima 22600 |
. . . . . 6
           MblFn

 
                               |
211 | 70, 49, 210 | syl2anc 667 |
. . . . 5
     
               |
212 | 211 | ad2antrr 733 |
. . . 4
             
           |
213 | 209, 212 | eqeltrrd 2532 |
. . 3
                 |
214 | 166, 213,
123, 122 | ltlecasei 9747 |
. 2
 

            |
215 | 3, 8, 124, 214 | ismbf2d 22609 |
1
   MblFn |