Proof of Theorem tfrlemibxssdm
Step | Hyp | Ref
| Expression |
1 | | tfrlemi1.5 |
. . 3
     
             |
2 | | tfrlemi1.4 |
. . . 4
   |
3 | | tfrlemisucfn.2 |
. . . . . . . . . . . 12
   
       |
4 | 3 | tfrlem3-2d 5869 |
. . . . . . . . . . 11
         |
5 | 4 | simprd 107 |
. . . . . . . . . 10
    
  |
6 | 5 | 3ad2ant1 924 |
. . . . . . . . 9
     
                  |
7 | | vex 2554 |
. . . . . . . . . . . . 13
 |
8 | | opexg 3955 |
. . . . . . . . . . . . 13
                |
9 | 7, 5, 8 | sylancr 393 |
. . . . . . . . . . . 12
          |
10 | | snidg 3392 |
. . . . . . . . . . . 12
       
                  |
11 | | elun2 3105 |
. . . . . . . . . . . 12
       
               
             |
12 | 9, 10, 11 | 3syl 17 |
. . . . . . . . . . 11
                     |
13 | 12 | 3ad2ant1 924 |
. . . . . . . . . 10
     
                  
             |
14 | | simp2r 930 |
. . . . . . . . . . . 12
     
              |
15 | | simp3l 931 |
. . . . . . . . . . . 12
     
              |
16 | | onelon 4087 |
. . . . . . . . . . . . . . 15
 
   |
17 | | rspe 2364 |
. . . . . . . . . . . . . . 15
  
    
        

    
         |
18 | 16, 17 | sylan 267 |
. . . . . . . . . . . . . 14
         
        

    
         |
19 | | tfrlemisucfn.1 |
. . . . . . . . . . . . . . 15


 
             |
20 | | vex 2554 |
. . . . . . . . . . . . . . 15
 |
21 | 19, 20 | tfrlem3a 5866 |
. . . . . . . . . . . . . 14
   
             |
22 | 18, 21 | sylibr 137 |
. . . . . . . . . . . . 13
         
       
  |
23 | 22 | 3adant1 921 |
. . . . . . . . . . . 12
     
              |
24 | 14, 15, 23 | 3jca 1083 |
. . . . . . . . . . 11
     
            
   |
25 | | snexg 3927 |
. . . . . . . . . . . . . 14
       
           |
26 | | unexg 4144 |
. . . . . . . . . . . . . . 15
            
            |
27 | 20, 26 | mpan 400 |
. . . . . . . . . . . . . 14
                       |
28 | 9, 25, 27 | 3syl 17 |
. . . . . . . . . . . . 13
              |
29 | | isset 2555 |
. . . . . . . . . . . . 13
                          |
30 | 28, 29 | sylib 127 |
. . . . . . . . . . . 12
               |
31 | 30 | 3ad2ant1 924 |
. . . . . . . . . . 11
     
            
             |
32 | | simpr3 911 |
. . . . . . . . . . . . . . 15
  
                          |
33 | | 19.8a 1479 |
. . . . . . . . . . . . . . . 16
 
                             |
34 | | rspe 2364 |
. . . . . . . . . . . . . . . . 17
                  
                 |
35 | | tfrlemi1.3 |
. . . . . . . . . . . . . . . . . 18


  
              |
36 | 35 | abeq2i 2145 |
. . . . . . . . . . . . . . . . 17
 
  
              |
37 | 34, 36 | sylibr 137 |
. . . . . . . . . . . . . . . 16
                    |
38 | 33, 37 | sylan2 270 |
. . . . . . . . . . . . . . 15
  
               |
39 | 32, 38 | eqeltrrd 2112 |
. . . . . . . . . . . . . 14
  
                          |
40 | 39 | 3exp2 1121 |
. . . . . . . . . . . . 13
  

           
               |
41 | 40 | 3imp 1097 |
. . . . . . . . . . . 12
   
                         |
42 | 41 | exlimdv 1697 |
. . . . . . . . . . 11
    

          
             |
43 | 24, 31, 42 | sylc 56 |
. . . . . . . . . 10
     
                         |
44 | | elunii 3576 |
. . . . . . . . . 10
                                      
   |
45 | 13, 43, 44 | syl2anc 391 |
. . . . . . . . 9
     
                  
   |
46 | | opeq2 3541 |
. . . . . . . . . . . 12
    
  
         |
47 | 46 | eleq1d 2103 |
. . . . . . . . . . 11
    
                |
48 | 47 | spcegv 2635 |
. . . . . . . . . 10
                       |
49 | 7 | eldm2 4476 |
. . . . . . . . . 10
          |
50 | 48, 49 | syl6ibr 151 |
. . . . . . . . 9
                  |
51 | 6, 45, 50 | sylc 56 |
. . . . . . . 8
     
               |
52 | 51 | 3expia 1105 |
. . . . . . 7
           
           |
53 | 52 | exlimdv 1697 |
. . . . . 6
         
               |
54 | 53 | anassrs 380 |
. . . . 5
         
               |
55 | 54 | ralimdva 2381 |
. . . 4
    
  
    
       
    |
56 | 2, 55 | mpdan 398 |
. . 3
              
   
    |
57 | 1, 56 | mpd 13 |
. 2
 
   |
58 | | dfss3 2929 |
. 2

 
   |
59 | 57, 58 | sylibr 137 |
1

   |