Proof of Theorem tfrlemibxssdm
| Step | Hyp | Ref
 | Expression | 
| 1 |   | tfrlemi1.5 | 
. . 3
                               
                      | 
| 2 |   | tfrlemi1.4 | 
. . . 4
              | 
| 3 |   | tfrlemisucfn.2 | 
. . . . . . . . . . . 12
               
            | 
| 4 | 3 | tfrlem3-2d 6370 | 
. . . . . . . . . . 11
                          | 
| 5 | 4 | simprd 114 | 
. . . . . . . . . 10
                  | 
| 6 | 5 | 3ad2ant1 1020 | 
. . . . . . . . 9
       
                                                                     | 
| 7 |   | vex 2766 | 
. . . . . . . . . . . . 13
        | 
| 8 |   | opexg 4261 | 
. . . . . . . . . . . . 13
                                         | 
| 9 | 7, 5, 8 | sylancr 414 | 
. . . . . . . . . . . 12
                       | 
| 10 |   | snidg 3651 | 
. . . . . . . . . . . 12
                   
                           | 
| 11 |   | elun2 3331 | 
. . . . . . . . . . . 12
                              
                                 | 
| 12 | 9, 10, 11 | 3syl 17 | 
. . . . . . . . . . 11
                                        | 
| 13 | 12 | 3ad2ant1 1020 | 
. . . . . . . . . 10
       
                                                                                           | 
| 14 |   | simp2r 1026 | 
. . . . . . . . . . . 12
       
                                                                 | 
| 15 |   | simp3l 1027 | 
. . . . . . . . . . . 12
       
                                                                 | 
| 16 |   | onelon 4419 | 
. . . . . . . . . . . . . . 15
               
            | 
| 17 |   | rspe 2546 | 
. . . . . . . . . . . . . . 15
                                                   
                      
                      | 
| 18 | 16, 17 | sylan 283 | 
. . . . . . . . . . . . . 14
                                     
                       
                      
                      | 
| 19 |   | tfrlemisucfn.1 | 
. . . . . . . . . . . . . . 15
               
                                        | 
| 20 |   | vex 2766 | 
. . . . . . . . . . . . . . 15
        | 
| 21 | 19, 20 | tfrlem3a 6368 | 
. . . . . . . . . . . . . 14
          
                      
                      | 
| 22 | 18, 21 | sylibr 134 | 
. . . . . . . . . . . . 13
                                     
                       
       | 
| 23 | 22 | 3adant1 1017 | 
. . . . . . . . . . . 12
       
                                                                 | 
| 24 | 14, 15, 23 | 3jca 1179 | 
. . . . . . . . . . 11
       
                                                                                   | 
| 25 |   | snexg 4217 | 
. . . . . . . . . . . . . 14
                   
                  | 
| 26 |   | unexg 4478 | 
. . . . . . . . . . . . . . 15
                          
                             | 
| 27 | 20, 26 | mpan 424 | 
. . . . . . . . . . . . . 14
                 
                            | 
| 28 | 9, 25, 27 | 3syl 17 | 
. . . . . . . . . . . . 13
                               | 
| 29 |   | isset 2769 | 
. . . . . . . . . . . . 13
                           
      
                    | 
| 30 | 28, 29 | sylib 122 | 
. . . . . . . . . . . 12
                                  | 
| 31 | 30 | 3ad2ant1 1020 | 
. . . . . . . . . . 11
       
                                                                                     | 
| 32 |   | simpr3 1007 | 
. . . . . . . . . . . . . . 15
                      
       
                                                 | 
| 33 |   | 19.8a 1604 | 
. . . . . . . . . . . . . . . 16
               
       
                                                                  | 
| 34 |   | rspe 2546 | 
. . . . . . . . . . . . . . . . 17
                                                                                                             | 
| 35 |   | tfrlemi1.3 | 
. . . . . . . . . . . . . . . . . 18
               
                                              | 
| 36 | 35 | abeq2i 2307 | 
. . . . . . . . . . . . . . . . 17
          
      
            
       
                       | 
| 37 | 34, 36 | sylibr 134 | 
. . . . . . . . . . . . . . . 16
                                                                 | 
| 38 | 33, 37 | sylan2 286 | 
. . . . . . . . . . . . . . 15
                      
       
                                | 
| 39 | 32, 38 | eqeltrrd 2274 | 
. . . . . . . . . . . . . 14
                      
       
                                                 | 
| 40 | 39 | 3exp2 1227 | 
. . . . . . . . . . . . 13
                                                                                  | 
| 41 | 40 | 3imp 1195 | 
. . . . . . . . . . . 12
               
       
                                                        | 
| 42 | 41 | exlimdv 1833 | 
. . . . . . . . . . 11
               
       
                                                           | 
| 43 | 24, 31, 42 | sylc 62 | 
. . . . . . . . . 10
       
                                                                                  | 
| 44 |   | elunii 3844 | 
. . . . . . . . . 10
                                                                                 | 
| 45 | 13, 43, 44 | syl2anc 411 | 
. . . . . . . . 9
       
                                                                           | 
| 46 |   | opeq2 3809 | 
. . . . . . . . . . . 12
                     
              | 
| 47 | 46 | eleq1d 2265 | 
. . . . . . . . . . 11
                             
                  | 
| 48 | 47 | spcegv 2852 | 
. . . . . . . . . 10
                                                  | 
| 49 | 7 | eldm2 4864 | 
. . . . . . . . . 10
                             | 
| 50 | 48, 49 | imbitrrdi 162 | 
. . . . . . . . 9
                                             | 
| 51 | 6, 45, 50 | sylc 62 | 
. . . . . . . 8
       
                                                                    | 
| 52 | 51 | 3expia 1207 | 
. . . . . . 7
       
                                   
                                  | 
| 53 | 52 | exlimdv 1833 | 
. . . . . 6
       
                                                                        | 
| 54 | 53 | anassrs 400 | 
. . . . 5
                                             
                                  | 
| 55 | 54 | ralimdva 2564 | 
. . . 4
       
      
       
                   
                                 
       | 
| 56 | 2, 55 | mpdan 421 | 
. . 3
                                                          
       
       | 
| 57 | 1, 56 | mpd 13 | 
. 2
                 
      | 
| 58 |   | dfss3 3173 | 
. 2
        
    
      
          | 
| 59 | 57, 58 | sylibr 134 | 
1
          
      |