Step | Hyp | Ref
| Expression |
1 | | elxpi 4644 |
. . . 4
           
    |
2 | | vex 2742 |
. . . . . . . 8
 |
3 | | vex 2742 |
. . . . . . . 8
 |
4 | 2, 3 | dfop 3779 |
. . . . . . 7
            |
5 | | snssi 3738 |
. . . . . . . . . . . . 13
     |
6 | | ssun3 3302 |
. . . . . . . . . . . . 13
     
   |
7 | 5, 6 | syl 14 |
. . . . . . . . . . . 12
       |
8 | 7 | adantr 276 |
. . . . . . . . . . 11
 
   
   |
9 | | sseq1 3180 |
. . . . . . . . . . 11
    
   
    |
10 | 8, 9 | syl5ibrcom 157 |
. . . . . . . . . 10
 
         |
11 | | df-pr 3601 |
. . . . . . . . . . . 12
          |
12 | | snssi 3738 |
. . . . . . . . . . . . . . 15
  
  |
13 | | ssun4 3303 |
. . . . . . . . . . . . . . 15
     
   |
14 | 12, 13 | syl 14 |
. . . . . . . . . . . . . 14
  
    |
15 | 7, 14 | anim12i 338 |
. . . . . . . . . . . . 13
 
     
       |
16 | | unss 3311 |
. . . . . . . . . . . . 13
    

    
      
   |
17 | 15, 16 | sylib 122 |
. . . . . . . . . . . 12
 
           |
18 | 11, 17 | eqsstrid 3203 |
. . . . . . . . . . 11
 
   
    |
19 | | sseq1 3180 |
. . . . . . . . . . 11
    
 
   
    |
20 | 18, 19 | syl5ibrcom 157 |
. . . . . . . . . 10
 
     
    |
21 | 10, 20 | jaod 717 |
. . . . . . . . 9
 
    
    
    |
22 | | vex 2742 |
. . . . . . . . . 10
 |
23 | 22 | elpr 3615 |
. . . . . . . . 9
    
      
      |
24 | 22 | elpw 3583 |
. . . . . . . . 9
   

   |
25 | 21, 23, 24 | 3imtr4g 205 |
. . . . . . . 8
 
                |
26 | 25 | ssrdv 3163 |
. . . . . . 7
 
          
   |
27 | 4, 26 | eqsstrid 3203 |
. . . . . 6
 
         |
28 | | sseq1 3180 |
. . . . . . 7
                 |
29 | 28 | biimpar 297 |
. . . . . 6
         
       |
30 | 27, 29 | sylan2 286 |
. . . . 5
     
 
     |
31 | 30 | exlimivv 1896 |
. . . 4
         
 
     |
32 | 1, 31 | syl 14 |
. . 3
        |
33 | 22 | elpw 3583 |
. . 3
   
      |
34 | 32, 33 | sylibr 134 |
. 2
         |
35 | 34 | ssriv 3161 |
1
       |