Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . . . . . 7
 
   |
2 | | simpl 109 |
. . . . . . 7
 
   |
3 | 1, 2 | fneq12d 5307 |
. . . . . 6
 
     |
4 | 1 | fveq1d 5516 |
. . . . . . . 8
 
           |
5 | 1 | reseq1d 4905 |
. . . . . . . . 9
 
       |
6 | 5 | fveq2d 5518 |
. . . . . . . 8
 
               |
7 | 4, 6 | eqeq12d 2192 |
. . . . . . 7
 
           
             |
8 | 2, 7 | raleqbidv 2684 |
. . . . . 6
 
            

             |
9 | 3, 8 | anbi12d 473 |
. . . . 5
 
   
                           |
10 | 9 | cbvexdva 1929 |
. . . 4
     
              
              |
11 | 10 | imbi2d 230 |
. . 3
  
                    
               |
12 | | fneq2 5304 |
. . . . . 6
 
   |
13 | | raleq 2672 |
. . . . . 6
  
         

             |
14 | 12, 13 | anbi12d 473 |
. . . . 5
                               |
15 | 14 | exbidv 1825 |
. . . 4
     
              
              |
16 | 15 | imbi2d 230 |
. . 3
  
                    
               |
17 | | r19.21v 2554 |
. . . 4
 
    
            

                  |
18 | | tfrlemisucfn.1 |
. . . . . . . . 9
 
               |
19 | 18 | tfrlem3 6309 |
. . . . . . . 8
 
               |
20 | | tfrlemisucfn.2 |
. . . . . . . . . 10
   
       |
21 | | fveq2 5514 |
. . . . . . . . . . . . 13
           |
22 | 21 | eleq1d 2246 |
. . . . . . . . . . . 12
     
       |
23 | 22 | anbi2d 464 |
. . . . . . . . . . 11
  
    
         |
24 | 23 | cbvalv 1917 |
. . . . . . . . . 10
                   |
25 | 20, 24 | sylib 122 |
. . . . . . . . 9
   
       |
26 | 25 | adantr 276 |
. . . . . . . 8
 
 
                   
       |
27 | | simpr 110 |
. . . . . . . . . . . . 13
       |
28 | | simplr 528 |
. . . . . . . . . . . . 13
       |
29 | 27, 28 | fneq12d 5307 |
. . . . . . . . . . . 12
     
   |
30 | 27 | eleq1d 2246 |
. . . . . . . . . . . 12
     
   |
31 | | simpll 527 |
. . . . . . . . . . . . 13
       |
32 | 27 | fveq2d 5518 |
. . . . . . . . . . . . . . . 16
               |
33 | 28, 32 | opeq12d 3786 |
. . . . . . . . . . . . . . 15
                     |
34 | 33 | sneqd 3605 |
. . . . . . . . . . . . . 14
                         |
35 | 27, 34 | uneq12d 3290 |
. . . . . . . . . . . . 13
                             |
36 | 31, 35 | eqeq12d 2192 |
. . . . . . . . . . . 12
                               |
37 | 29, 30, 36 | 3anbi123d 1312 |
. . . . . . . . . . 11
      
                            |
38 | 37 | cbvexdva 1929 |
. . . . . . . . . 10
 
    
           
  
               |
39 | 38 | cbvrexdva 2713 |
. . . . . . . . 9
  
              

  
               |
40 | 39 | cbvabv 2302 |
. . . . . . . 8
    
                 
              |
41 | | simpl 109 |
. . . . . . . . 9
      
           
  |
42 | 41 | adantl 277 |
. . . . . . . 8
 
 
                   |
43 | | simpr 110 |
. . . . . . . . . 10
      
           

                 |
44 | | simpr 110 |
. . . . . . . . . . . . . 14
 
   |
45 | | simpl 109 |
. . . . . . . . . . . . . 14
 
   |
46 | 44, 45 | fneq12d 5307 |
. . . . . . . . . . . . 13
 
     |
47 | | simplr 528 |
. . . . . . . . . . . . . . . 16
       |
48 | | simpr 110 |
. . . . . . . . . . . . . . . 16
       |
49 | 47, 48 | fveq12d 5521 |
. . . . . . . . . . . . . . 15
               |
50 | 47, 48 | reseq12d 4907 |
. . . . . . . . . . . . . . . 16
           |
51 | 50 | fveq2d 5518 |
. . . . . . . . . . . . . . 15
                   |
52 | 49, 51 | eqeq12d 2192 |
. . . . . . . . . . . . . 14
               
             |
53 | | simpll 527 |
. . . . . . . . . . . . . 14
       |
54 | 52, 53 | cbvraldva2 2710 |
. . . . . . . . . . . . 13
 
            

             |
55 | 46, 54 | anbi12d 473 |
. . . . . . . . . . . 12
 
   
                           |
56 | 55 | cbvexdva 1929 |
. . . . . . . . . . 11
     
              
              |
57 | 56 | cbvralv 2703 |
. . . . . . . . . 10
 
   
           
   
             |
58 | 43, 57 | sylib 122 |
. . . . . . . . 9
      
           

                 |
59 | 58 | adantl 277 |
. . . . . . . 8
 
 
                 
                 |
60 | 19, 26, 40, 42, 59 | tfrlemiex 6329 |
. . . . . . 7
 
 
                                  |
61 | 60 | expr 375 |
. . . . . 6
 

 
   
              
              |
62 | 61 | expcom 116 |
. . . . 5
   
                  
               |
63 | 62 | a2d 26 |
. . . 4
  

               
    
               |
64 | 17, 63 | biimtrid 152 |
. . 3
  

               
    
               |
65 | 11, 16, 64 | tfis3 4584 |
. 2
     
              |
66 | 65 | impcom 125 |
1
 

                 |