Step | Hyp | Ref
| Expression |
1 | | ufilfil 20997 |
. . 3
    
      |
2 | | ufilmax 21000 |
. . . . 5
         

  |
3 | 2 | 3expia 1233 |
. . . 4
               |
4 | 3 | ralrimiva 2809 |
. . 3
    
          |
5 | 1, 4 | jca 541 |
. 2
    
    
           |
6 | | simpl 464 |
. . 3
      
              |
7 | | selpw 3949 |
. . . . 5
 
  |
8 | | simpll 768 |
. . . . . . . . . . . . . . . 16
       

  
      |
9 | | snex 4641 |
. . . . . . . . . . . . . . . 16
 
 |
10 | | unexg 6611 |
. . . . . . . . . . . . . . . 16
               |
11 | 8, 9, 10 | sylancl 675 |
. . . . . . . . . . . . . . 15
       

         |
12 | | ssfii 7951 |
. . . . . . . . . . . . . . 15
                   |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
       

                 |
14 | | filsspw 20944 |
. . . . . . . . . . . . . . . . . 18
    
   |
15 | 14 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
       

      |
16 | 7 | biimpri 211 |
. . . . . . . . . . . . . . . . . . 19
    |
17 | 16 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . 18
       

  
   |
18 | 17 | snssd 4108 |
. . . . . . . . . . . . . . . . 17
       

        |
19 | 15, 18 | unssd 3601 |
. . . . . . . . . . . . . . . 16
       

          |
20 | | ssun2 3589 |
. . . . . . . . . . . . . . . . . 18
       |
21 | | vex 3034 |
. . . . . . . . . . . . . . . . . . 19
 |
22 | 21 | snnz 4081 |
. . . . . . . . . . . . . . . . . 18
   |
23 | | ssn0 3770 |
. . . . . . . . . . . . . . . . . 18
    
            |
24 | 20, 22, 23 | mp2an 686 |
. . . . . . . . . . . . . . . . 17
     |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . 16
       

         |
26 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
       

   
    |
27 | | ineq2 3619 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
28 | 27 | neeq1d 2702 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
29 | 21, 28 | ralsn 4001 |
. . . . . . . . . . . . . . . . . . 19
 
   
    |
30 | 29 | ralbii 2823 |
. . . . . . . . . . . . . . . . . 18
 

   

    |
31 | 26, 30 | sylibr 217 |
. . . . . . . . . . . . . . . . 17
       

   

      |
32 | | filfbas 20941 |
. . . . . . . . . . . . . . . . . . 19
    
      |
33 | 32 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
       

  
      |
34 | | simplr 770 |
. . . . . . . . . . . . . . . . . . 19
       

     |
35 | | inss2 3644 |
. . . . . . . . . . . . . . . . . . . 20
   |
36 | | filtop 20948 |
. . . . . . . . . . . . . . . . . . . . . 22
    
  |
37 | 36 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
         |
38 | | ineq1 3618 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
39 | 38 | neeq1d 2702 |
. . . . . . . . . . . . . . . . . . . . . 22
   
     |
40 | 39 | rspcva 3134 |
. . . . . . . . . . . . . . . . . . . . 21
          |
41 | 37, 40 | sylan 479 |
. . . . . . . . . . . . . . . . . . . 20
       

       |
42 | | ssn0 3770 |
. . . . . . . . . . . . . . . . . . . 20
   

    |
43 | 35, 41, 42 | sylancr 676 |
. . . . . . . . . . . . . . . . . . 19
       

     |
44 | 36 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
       

  
  |
45 | | snfbas 20959 |
. . . . . . . . . . . . . . . . . . 19
 
  
      |
46 | 34, 43, 44, 45 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
       

           |
47 | | fbunfip 20962 |
. . . . . . . . . . . . . . . . . 18
            
    
   

   
    |
48 | 33, 46, 47 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
       

           

   
    |
49 | 31, 48 | mpbird 240 |
. . . . . . . . . . . . . . . 16
       

             |
50 | | fsubbas 20960 |
. . . . . . . . . . . . . . . . 17
     
            
                 |
51 | 44, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
       

       
            
                 |
52 | 19, 25, 49, 51 | mpbir3and 1213 |
. . . . . . . . . . . . . . 15
       

      
          |
53 | | ssfg 20965 |
. . . . . . . . . . . . . . 15
                
          
       |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . 14
       

      
          
       |
55 | 13, 54 | sstrd 3428 |
. . . . . . . . . . . . 13
       

             
       |
56 | 55 | unssad 3602 |
. . . . . . . . . . . 12
       

                 |
57 | | fgcl 20971 |
. . . . . . . . . . . . 13
                               |
58 | | sseq2 3440 |
. . . . . . . . . . . . . . 15
                             |
59 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
                    
        |
60 | 58, 59 | imbi12d 327 |
. . . . . . . . . . . . . 14
                       
           
         |
61 | 60 | rspcv 3132 |
. . . . . . . . . . . . 13
       
        
 
              
           
         |
62 | 52, 57, 61 | 3syl 18 |
. . . . . . . . . . . 12
       

           
            
      
         |
63 | 56, 62 | mpid 41 |
. . . . . . . . . . 11
       

           
      
        |
64 | | ssnid 3989 |
. . . . . . . . . . . . . . 15
   |
65 | 20, 64 | sselii 3415 |
. . . . . . . . . . . . . 14
     |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
       

  
      |
67 | 55, 66 | sseldd 3419 |
. . . . . . . . . . . 12
       

  
      
       |
68 | | eleq2 2538 |
. . . . . . . . . . . 12
                             |
69 | 67, 68 | syl5ibrcom 230 |
. . . . . . . . . . 11
       

          
        |
70 | 63, 69 | syld 44 |
. . . . . . . . . 10
       

           
   |
71 | 70 | impancom 447 |
. . . . . . . . 9
       
          
     |
72 | 71 | an32s 821 |
. . . . . . . 8
                  
     |
73 | 72 | con3d 140 |
. . . . . . 7
                 
      |
74 | | rexnal 2836 |
. . . . . . . . 9
   

    |
75 | | nne 2647 |
. . . . . . . . . . 11
  
    |
76 | | filelss 20945 |
. . . . . . . . . . . . 13
         |
77 | | reldisj 3812 |
. . . . . . . . . . . . 13
   

    |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . 12
         

    |
79 | | difss 3549 |
. . . . . . . . . . . . . 14
   |
80 | | filss 20946 |
. . . . . . . . . . . . . . 15
       

        |
81 | 80 | 3exp2 1251 |
. . . . . . . . . . . . . 14
    

   
         |
82 | 79, 81 | mpii 43 |
. . . . . . . . . . . . 13
    

         |
83 | 82 | imp 436 |
. . . . . . . . . . . 12
       
       |
84 | 78, 83 | sylbid 223 |
. . . . . . . . . . 11
               |
85 | 75, 84 | syl5bi 225 |
. . . . . . . . . 10
               |
86 | 85 | rexlimdva 2871 |
. . . . . . . . 9
    
 
       |
87 | 74, 86 | syl5bir 226 |
. . . . . . . 8
    
   
     |
88 | 87 | ad2antrr 740 |
. . . . . . 7
                          |
89 | 73, 88 | syld 44 |
. . . . . 6
                 
     |
90 | 89 | orrd 385 |
. . . . 5
                  
    |
91 | 7, 90 | sylan2b 483 |
. . . 4
                        |
92 | 91 | ralrimiva 2809 |
. . 3
      
                |
93 | | isufil 20996 |
. . 3
         
         |
94 | 6, 92, 93 | sylanbrc 677 |
. 2
      
              |
95 | 5, 94 | impbii 192 |
1
         
           |