Step | Hyp | Ref
| Expression |
1 | | tfrlemi1.5 |
. . 3
     
             |
2 | | tfrlemi1.4 |
. . . 4
   |
3 | | tfrlemisucfn.2 |
. . . . . . . . . . . 12
   
       |
4 | 3 | tfrlem3-2d 6313 |
. . . . . . . . . . 11
         |
5 | 4 | simprd 114 |
. . . . . . . . . 10
       |
6 | 5 | 3ad2ant1 1018 |
. . . . . . . . 9
 
                      |
7 | | vex 2741 |
. . . . . . . . . . . . 13
 |
8 | | opexg 4229 |
. . . . . . . . . . . . 13
                |
9 | 7, 5, 8 | sylancr 414 |
. . . . . . . . . . . 12
          |
10 | | snidg 3622 |
. . . . . . . . . . . 12
       
                  |
11 | | elun2 3304 |
. . . . . . . . . . . 12
                
                    |
12 | 9, 10, 11 | 3syl 17 |
. . . . . . . . . . 11
                     |
13 | 12 | 3ad2ant1 1018 |
. . . . . . . . . 10
 
                                    |
14 | | simp2r 1024 |
. . . . . . . . . . . 12
 
                  |
15 | | simp3l 1025 |
. . . . . . . . . . . 12
 
                  |
16 | | onelon 4385 |
. . . . . . . . . . . . . . 15
 
   |
17 | | rspe 2526 |
. . . . . . . . . . . . . . 15
               
  
             |
18 | 16, 17 | sylan 283 |
. . . . . . . . . . . . . 14
     
           
  
             |
19 | | tfrlemisucfn.1 |
. . . . . . . . . . . . . . 15
 
               |
20 | | vex 2741 |
. . . . . . . . . . . . . . 15
 |
21 | 19, 20 | tfrlem3a 6311 |
. . . . . . . . . . . . . 14

  
             |
22 | 18, 21 | sylibr 134 |
. . . . . . . . . . . . 13
     
           
  |
23 | 22 | 3adant1 1015 |
. . . . . . . . . . . 12
 
                  |
24 | 14, 15, 23 | 3jca 1177 |
. . . . . . . . . . 11
 
                    |
25 | | snexg 4185 |
. . . . . . . . . . . . . 14
       
           |
26 | | unexg 4444 |
. . . . . . . . . . . . . . 15
          
              |
27 | 20, 26 | mpan 424 |
. . . . . . . . . . . . . 14
         
             |
28 | 9, 25, 27 | 3syl 17 |
. . . . . . . . . . . . 13
              |
29 | | isset 2744 |
. . . . . . . . . . . . 13
           

             |
30 | 28, 29 | sylib 122 |
. . . . . . . . . . . 12
               |
31 | 30 | 3ad2ant1 1018 |
. . . . . . . . . . 11
 
                              |
32 | | simpr3 1005 |
. . . . . . . . . . . . . . 15
  
                          |
33 | | 19.8a 1590 |
. . . . . . . . . . . . . . . 16
 
                             |
34 | | rspe 2526 |
. . . . . . . . . . . . . . . . 17
                                    |
35 | | tfrlemi1.3 |
. . . . . . . . . . . . . . . . . 18
 
                 |
36 | 35 | abeq2i 2288 |
. . . . . . . . . . . . . . . . 17


  
              |
37 | 34, 36 | sylibr 134 |
. . . . . . . . . . . . . . . 16
                    |
38 | 33, 37 | sylan2 286 |
. . . . . . . . . . . . . . 15
  
               |
39 | 32, 38 | eqeltrrd 2255 |
. . . . . . . . . . . . . 14
  
                          |
40 | 39 | 3exp2 1225 |
. . . . . . . . . . . . 13
                               |
41 | 40 | 3imp 1193 |
. . . . . . . . . . . 12
 
                           |
42 | 41 | exlimdv 1819 |
. . . . . . . . . . 11
 
                            |
43 | 24, 31, 42 | sylc 62 |
. . . . . . . . . 10
 
                             |
44 | | elunii 3815 |
. . . . . . . . . 10
                                          |
45 | 13, 43, 44 | syl2anc 411 |
. . . . . . . . 9
 
                          |
46 | | opeq2 3780 |
. . . . . . . . . . . 12
       
         |
47 | 46 | eleq1d 2246 |
. . . . . . . . . . 11
         
           |
48 | 47 | spcegv 2826 |
. . . . . . . . . 10
                       |
49 | 7 | eldm2 4826 |
. . . . . . . . . 10
          |
50 | 48, 49 | imbitrrdi 162 |
. . . . . . . . 9
                  |
51 | 6, 45, 50 | sylc 62 |
. . . . . . . 8
 
                   |
52 | 51 | 3expia 1205 |
. . . . . . 7
 
     
               |
53 | 52 | exlimdv 1819 |
. . . . . 6
 
                       |
54 | 53 | anassrs 400 |
. . . . 5
         
               |
55 | 54 | ralimdva 2544 |
. . . 4
 

 
   
           
    |
56 | 2, 55 | mpdan 421 |
. . 3
                  
    |
57 | 1, 56 | mpd 13 |
. 2
 
   |
58 | | dfss3 3146 |
. 2



   |
59 | 57, 58 | sylibr 134 |
1

   |