Step | Hyp | Ref
| Expression |
1 | | dmres 4575 |
. . . . 5
     |
2 | 1 | imaeq2i 4609 |
. . . 4
  
      
   |
3 | | imadmres 4756 |
. . . 4
  
        |
4 | 2, 3 | eqtr3i 2059 |
. . 3
           |
5 | 4 | sseq2i 2964 |
. 2
    
 
      |
6 | | ssrab2 3019 |
. . . 4
        
  |
7 | | ssel2 2934 |
. . . . . . . . 9
 
          
    |
8 | 7 | adantll 445 |
. . . . . . . 8
      
       
    |
9 | | fvelima 5168 |
. . . . . . . . . . . 12
     
  
       
  |
10 | 9 | ex 108 |
. . . . . . . . . . 11

    
         
   |
11 | 10 | adantr 261 |
. . . . . . . . . 10
   
      
          |
12 | | eleq1a 2106 |
. . . . . . . . . . . . . . . 16
             |
13 | 12 | anim2d 320 |
. . . . . . . . . . . . . . 15
  

    
       
    |
14 | | fveq2 5121 |
. . . . . . . . . . . . . . . . 17
           |
15 | 14 | eleq1d 2103 |
. . . . . . . . . . . . . . . 16
             |
16 | 15 | elrab 2692 |
. . . . . . . . . . . . . . 15
                   |
17 | 13, 16 | syl6ibr 151 |
. . . . . . . . . . . . . 14
  

    
            |
18 | | simpr 103 |
. . . . . . . . . . . . . . 15
  
    
    
  |
19 | 18 | a1i 9 |
. . . . . . . . . . . . . 14
  

    
    
   |
20 | 17, 19 | jcad 291 |
. . . . . . . . . . . . 13
  

    
  
     
    
    |
21 | 20 | reximdv2 2412 |
. . . . . . . . . . . 12
  

      
               |
22 | 21 | adantl 262 |
. . . . . . . . . . 11
    

      
               |
23 | | funfn 4874 |
. . . . . . . . . . . . 13
   |
24 | | inss2 3152 |
. . . . . . . . . . . . . . 15

  |
25 | 6, 24 | sstri 2948 |
. . . . . . . . . . . . . 14
         |
26 | | fvelimab 5172 |
. . . . . . . . . . . . . 14
    
                    
     
        |
27 | 25, 26 | mpan2 401 |
. . . . . . . . . . . . 13
 
               
        
   |
28 | 23, 27 | sylbi 114 |
. . . . . . . . . . . 12

    
     
   
     
        |
29 | 28 | adantr 261 |
. . . . . . . . . . 11
   
     
     
   
        
   |
30 | 22, 29 | sylibrd 158 |
. . . . . . . . . 10
    

         
     
     |
31 | 11, 30 | syld 40 |
. . . . . . . . 9
   
         
     
     |
32 | 31 | adantlr 446 |
. . . . . . . 8
      
    
         
     
     |
33 | 8, 32 | mpd 13 |
. . . . . . 7
      
       
     
    |
34 | 33 | ex 108 |
. . . . . 6
     
  

     
         |
35 | | fvelima 5168 |
. . . . . . . . 9
     
     
  
   
        
  |
36 | 35 | ex 108 |
. . . . . . . 8

    
     
     
        
   |
37 | | eleq1 2097 |
. . . . . . . . . . . 12
             |
38 | 37 | biimpcd 148 |
. . . . . . . . . . 11
             |
39 | 38 | adantl 262 |
. . . . . . . . . 10
  
    
     
   |
40 | 16, 39 | sylbi 114 |
. . . . . . . . 9
                 |
41 | 40 | rexlimiv 2421 |
. . . . . . . 8
 
              |
42 | 36, 41 | syl6 29 |
. . . . . . 7

    
     
     |
43 | 42 | adantr 261 |
. . . . . 6
     
  

     
     
   |
44 | 34, 43 | impbid 120 |
. . . . 5
     
  

   
     
     |
45 | 44 | eqrdv 2035 |
. . . 4
     
  
              |
46 | | ssimaex.1 |
. . . . . . 7
 |
47 | 46 | inex1 3882 |
. . . . . 6

  |
48 | 47 | rabex 3892 |
. . . . 5
         |
49 | | sseq1 2960 |
. . . . . 6
                    
    |
50 | | imaeq2 4607 |
. . . . . . 7
                
     
    |
51 | 50 | eqeq2d 2048 |
. . . . . 6
         
                   |
52 | 49, 51 | anbi12d 442 |
. . . . 5
          

               
                 |
53 | 48, 52 | spcev 2641 |
. . . 4
    
          
     
  
  

        |
54 | 6, 45, 53 | sylancr 393 |
. . 3
     
  
  

        |
55 | | inss1 3151 |
. . . . . 6

  |
56 | | sstr 2947 |
. . . . . 6
 
  
    |
57 | 55, 56 | mpan2 401 |
. . . . 5
     |
58 | 57 | anim1i 323 |
. . . 4
 
 
     
       |
59 | 58 | eximi 1488 |
. . 3
    
                |
60 | 54, 59 | syl 14 |
. 2
     
  
  
       |
61 | 5, 60 | sylan2br 272 |
1
      
  
       |