Step | Hyp | Ref
| Expression |
1 | | n0 3741 |
. . 3
    |
2 | | snssi 4116 |
. . . . . . . . . . . 12
  
  |
3 | 2 | anim2i 573 |
. . . . . . . . . . 11
    
        |
4 | | ssin 3654 |
. . . . . . . . . . . 12
      
      |
5 | | vex 3048 |
. . . . . . . . . . . . 13
 |
6 | 5 | snss 4096 |
. . . . . . . . . . . 12
  
      |
7 | 4, 6 | bitr4i 256 |
. . . . . . . . . . 11
      
    |
8 | 3, 7 | sylib 200 |
. . . . . . . . . 10
    
    |
9 | | ne0i 3737 |
. . . . . . . . . 10
   
   |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
    
    |
11 | | inss2 3653 |
. . . . . . . . . . . 12
   |
12 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
13 | 12 | inex1 4544 |
. . . . . . . . . . . . 13
   |
14 | 13 | epfrc 4820 |
. . . . . . . . . . . 12
  
   

        |
15 | 11, 14 | mp3an2 1352 |
. . . . . . . . . . 11
    

        |
16 | | elin 3617 |
. . . . . . . . . . . . . . 15
  

   |
17 | 16 | anbi1i 701 |
. . . . . . . . . . . . . 14
        
 
        |
18 | | anass 655 |
. . . . . . . . . . . . . 14
   
 
             |
19 | 17, 18 | bitri 253 |
. . . . . . . . . . . . 13
        

         |
20 | | n0 3741 |
. . . . . . . . . . . . . . . . . . 19
        |
21 | | inss1 3652 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
22 | 21 | sseli 3428 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
23 | 22 | ancri 555 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
24 | | trel 4504 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

 
    |
25 | | inass 3642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         |
26 | | incom 3625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     |
27 | 26 | ineq2i 3631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
   |
28 | 25, 27 | eqtri 2473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
   |
29 | 28 | eleq2i 2521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
 
    |
30 | | elin 3617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    

     |
31 | 29, 30 | bitr2i 254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  
      |
32 | | ne0i 3737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
   |
33 | 31, 32 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
         |
34 | 33 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
35 | 24, 34 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . 24

 
            |
36 | 35 | expd 438 |
. . . . . . . . . . . . . . . . . . . . . . 23


             |
37 | 36 | com34 86 |
. . . . . . . . . . . . . . . . . . . . . 22


             |
38 | 37 | impd 433 |
. . . . . . . . . . . . . . . . . . . . 21

 
            |
39 | 23, 38 | syl5 33 |
. . . . . . . . . . . . . . . . . . . 20

  

        |
40 | 39 | exlimdv 1779 |
. . . . . . . . . . . . . . . . . . 19

 

          |
41 | 20, 40 | syl5bi 221 |
. . . . . . . . . . . . . . . . . 18

 


        |
42 | 41 | com23 81 |
. . . . . . . . . . . . . . . . 17


  
 
      |
43 | 42 | imp 431 |
. . . . . . . . . . . . . . . 16
        
    |
44 | 43 | necon4d 2648 |
. . . . . . . . . . . . . . 15
        
    |
45 | 44 | anim2d 569 |
. . . . . . . . . . . . . 14
                 |
46 | 45 | expimpd 608 |
. . . . . . . . . . . . 13

  
             |
47 | 19, 46 | syl5bi 221 |
. . . . . . . . . . . 12

                |
48 | 47 | reximdv2 2858 |
. . . . . . . . . . 11

 
        
    |
49 | 15, 48 | syl5 33 |
. . . . . . . . . 10

 
  
     |
50 | 49 | expcomd 440 |
. . . . . . . . 9

 


      |
51 | 10, 50 | syl5 33 |
. . . . . . . 8

    

      |
52 | 51 | expd 438 |
. . . . . . 7

     
      |
53 | 52 | impcom 432 |
. . . . . 6
     

      |
54 | 53 | 3adant3 1028 |
. . . . 5
          
 


      |
55 | | snex 4641 |
. . . . . 6
   |
56 | 55 | tz9.1 8213 |
. . . . 5
               |
57 | 54, 56 | exlimiiv 1777 |
. . . 4
 
     |
58 | 57 | exlimiv 1776 |
. . 3
   
    |
59 | 1, 58 | sylbi 199 |
. 2


     |
60 | 59 | impcom 432 |
1
  
    |