Step | Hyp | Ref
| Expression |
1 | | vex 3060 |
. . . . 5
 |
2 | 1 | elintrab 4260 |
. . . 4
       
          |
3 | | filsspw 20915 |
. . . . . . . . . . . . . 14
    
   |
4 | 3 | 3ad2ant1 1035 |
. . . . . . . . . . . . 13
     
    |
5 | | difss 3572 |
. . . . . . . . . . . . . . 15
   |
6 | | filtop 20919 |
. . . . . . . . . . . . . . . . . 18
    
  |
7 | | difexg 4565 |
. . . . . . . . . . . . . . . . . 18
     |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
    
    |
9 | 8 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . 16
     
     |
10 | | elpwg 3971 |
. . . . . . . . . . . . . . . 16
            |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . 15
     
      
   |
12 | 5, 11 | mpbiri 241 |
. . . . . . . . . . . . . 14
     
      |
13 | 12 | snssd 4130 |
. . . . . . . . . . . . 13
     
        |
14 | 4, 13 | unssd 3622 |
. . . . . . . . . . . 12
     
          |
15 | | ssun1 3609 |
. . . . . . . . . . . . . 14

      |
16 | | filn0 20926 |
. . . . . . . . . . . . . 14
    
  |
17 | | ssn0 3779 |
. . . . . . . . . . . . . 14
 
               |
18 | 15, 16, 17 | sylancr 674 |
. . . . . . . . . . . . 13
    
        |
19 | 18 | 3ad2ant1 1035 |
. . . . . . . . . . . 12
     
         |
20 | | elsni 4005 |
. . . . . . . . . . . . . . 15
         |
21 | | filelss 20916 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
22 | 21 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
   |
23 | | reldisj 3820 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
       |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
     
       |
25 | | dfss4 3689 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

      |
26 | 25 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
27 | 26 | sseq2d 3472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   
   |
28 | 27 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
 
   
   |
29 | 24, 28 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . . 22
     
     
   |
30 | | filss 20917 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
  |
31 | 30 | 3exp2 1235 |
. . . . . . . . . . . . . . . . . . . . . . 23
    

 
     |
32 | 31 | 3imp 1208 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 
   |
33 | 29, 32 | sylbid 223 |
. . . . . . . . . . . . . . . . . . . . 21
     
     
   |
34 | 33 | necon3bd 2650 |
. . . . . . . . . . . . . . . . . . . 20
     
 
       |
35 | 34 | 3exp 1214 |
. . . . . . . . . . . . . . . . . . 19
    

 
         |
36 | 35 | com24 90 |
. . . . . . . . . . . . . . . . . 18
    


          |
37 | 36 | 3imp1 1230 |
. . . . . . . . . . . . . . . . 17
         
     |
38 | | ineq2 3640 |
. . . . . . . . . . . . . . . . . 18
   
       |
39 | 38 | neeq1d 2695 |
. . . . . . . . . . . . . . . . 17
     
       |
40 | 37, 39 | syl5ibrcom 230 |
. . . . . . . . . . . . . . . 16
                 |
41 | 40 | expimpd 612 |
. . . . . . . . . . . . . . 15
     
      
    |
42 | 20, 41 | sylan2i 665 |
. . . . . . . . . . . . . 14
     
             |
43 | 42 | ralrimivv 2820 |
. . . . . . . . . . . . 13
     
 

        |
44 | | filfbas 20912 |
. . . . . . . . . . . . . . 15
    
      |
45 | 44 | 3ad2ant1 1035 |
. . . . . . . . . . . . . 14
     

      |
46 | 5 | a1i 11 |
. . . . . . . . . . . . . . 15
     
  
  |
47 | 26 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . . . . . . . . 22
        
      |
48 | | difeq2 3557 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
        |
49 | | dif0 3849 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
50 | 48, 49 | syl6eq 2512 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
      |
51 | 50 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . . . . . . 22
        
      |
52 | 47, 51 | eqtr3d 2498 |
. . . . . . . . . . . . . . . . . . . . 21
        
  |
53 | 6 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . . . 21
        
  |
54 | 52, 53 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . . 20
        
  |
55 | 54 | 3expia 1217 |
. . . . . . . . . . . . . . . . . . 19
             |
56 | 55 | necon3bd 2650 |
. . . . . . . . . . . . . . . . . 18
       
     |
57 | 56 | ex 440 |
. . . . . . . . . . . . . . . . 17
    


      |
58 | 57 | com23 81 |
. . . . . . . . . . . . . . . 16
    


      |
59 | 58 | 3imp 1208 |
. . . . . . . . . . . . . . 15
     
     |
60 | 6 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . 15
     

  |
61 | | snfbas 20930 |
. . . . . . . . . . . . . . 15
   

            |
62 | 46, 59, 60, 61 | syl3anc 1276 |
. . . . . . . . . . . . . 14
     
           |
63 | | fbunfip 20933 |
. . . . . . . . . . . . . 14
              
    
     

     
    |
64 | 45, 62, 63 | syl2anc 671 |
. . . . . . . . . . . . 13
     
           

     
    |
65 | 43, 64 | mpbird 240 |
. . . . . . . . . . . 12
     
             |
66 | | fsubbas 20931 |
. . . . . . . . . . . . . 14
     
                 

        
          |
67 | 6, 66 | syl 17 |
. . . . . . . . . . . . 13
    
                     
                     |
68 | 67 | 3ad2ant1 1035 |
. . . . . . . . . . . 12
     
     
                
                     |
69 | 14, 19, 65, 68 | mpbir3and 1197 |
. . . . . . . . . . 11
     
    
            |
70 | | fgcl 20942 |
. . . . . . . . . . 11
                                   |
71 | 69, 70 | syl 17 |
. . . . . . . . . 10
     
                     |
72 | | filssufil 20976 |
. . . . . . . . . . 11
       
          
                      |
73 | | snex 4655 |
. . . . . . . . . . . . . . . . . . . . 21
     |
74 | | unexg 6619 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
75 | 73, 74 | mpan2 682 |
. . . . . . . . . . . . . . . . . . . 20
    
        |
76 | | ssfii 7959 |
. . . . . . . . . . . . . . . . . . . 20
                         |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    
         
        |
78 | 77 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . 18
     
                   |
79 | 78 | unssad 3623 |
. . . . . . . . . . . . . . . . 17
     
    
        |
80 | | ssfg 20936 |
. . . . . . . . . . . . . . . . . 18
                  
            
         |
81 | 69, 80 | syl 17 |
. . . . . . . . . . . . . . . . 17
     
    
            
         |
82 | 79, 81 | sstrd 3454 |
. . . . . . . . . . . . . . . 16
     
                 |
83 | 82 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
       
            
                        |
84 | | simpr 467 |
. . . . . . . . . . . . . . 15
       
            
                     
  |
85 | 83, 84 | sstrd 3454 |
. . . . . . . . . . . . . 14
       
            
          |
86 | | ufilfil 20968 |
. . . . . . . . . . . . . . . . 17
    
      |
87 | | 0nelfil 20913 |
. . . . . . . . . . . . . . . . 17
    
  |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
    
  |
89 | 88 | ad2antlr 738 |
. . . . . . . . . . . . . . 15
       
            
          |
90 | | disjdif 3851 |
. . . . . . . . . . . . . . . . 17
     |
91 | 86 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . 18
       
                    
 
      |
92 | | simprr 771 |
. . . . . . . . . . . . . . . . . 18
       
                    
 
  |
93 | 77 | unssbd 3624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
       
        |
94 | 93 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                 |
95 | 94 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
                
            |
96 | 69 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             |
97 | 96, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
                                       |
98 | 95, 97 | sstrd 3454 |
. . . . . . . . . . . . . . . . . . . . 21
                
      
         |
99 | 98 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
       
                    
 
                    |
100 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . 20
       
                    
 
      
         |
101 | 99, 100 | sstrd 3454 |
. . . . . . . . . . . . . . . . . . 19
       
                    
 
      |
102 | | snidg 4006 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
103 | 8, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
    
        |
104 | 103 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . . 20
     
         |
105 | 104 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
       
                    
 
        |
106 | 101, 105 | sseldd 3445 |
. . . . . . . . . . . . . . . . . 18
       
                    
 
    |
107 | | filin 20918 |
. . . . . . . . . . . . . . . . . 18
     
   
     |
108 | 91, 92, 106, 107 | syl3anc 1276 |
. . . . . . . . . . . . . . . . 17
       
                    
 
      |
109 | 90, 108 | syl5eqelr 2545 |
. . . . . . . . . . . . . . . 16
       
                    
 
  |
110 | 109 | expr 624 |
. . . . . . . . . . . . . . 15
       
            
            |
111 | 89, 110 | mtod 182 |
. . . . . . . . . . . . . 14
       
            
       
  |
112 | 85, 111 | jca 539 |
. . . . . . . . . . . . 13
       
            
            |
113 | 112 | exp31 613 |
. . . . . . . . . . . 12
     
                           |
114 | 113 | reximdvai 2871 |
. . . . . . . . . . 11
     
                                 |
115 | 72, 114 | syl5 33 |
. . . . . . . . . 10
     
                   
           |
116 | 71, 115 | mpd 15 |
. . . . . . . . 9
     
 
     
   |
117 | 116 | 3expia 1217 |
. . . . . . . 8
     
             |
118 | | filssufil 20976 |
. . . . . . . . . 10
    
        |
119 | | filelss 20916 |
. . . . . . . . . . . . . . . . 17
         |
120 | 119 | ex 440 |
. . . . . . . . . . . . . . . 16
    

   |
121 | 86, 120 | syl 17 |
. . . . . . . . . . . . . . 15
    

   |
122 | 121 | con3d 140 |
. . . . . . . . . . . . . 14
    

   |
123 | 122 | impcom 436 |
. . . . . . . . . . . . 13
 
    
  |
124 | 123 | a1d 26 |
. . . . . . . . . . . 12
 
     
   |
125 | 124 | ancld 560 |
. . . . . . . . . . 11
 
           |
126 | 125 | reximdva 2874 |
. . . . . . . . . 10

                  |
127 | 118, 126 | syl5com 31 |
. . . . . . . . 9
    
            |
128 | 127 | adantr 471 |
. . . . . . . 8
     
             |
129 | 117, 128 | pm2.61d 163 |
. . . . . . 7
     
           |
130 | 129 | ex 440 |
. . . . . 6
    

      
    |
131 | | rexanali 2852 |
. . . . . 6
       
           |
132 | 130, 131 | syl6ib 234 |
. . . . 5
    

           |
133 | 132 | con4d 109 |
. . . 4
    
 
          |
134 | 2, 133 | syl5bi 225 |
. . 3
    
       
   |
135 | 134 | ssrdv 3450 |
. 2
    
      
  |
136 | | ssintub 4266 |
. . 3
     
  |
137 | 136 | a1i 11 |
. 2
    
         |
138 | 135, 137 | eqssd 3461 |
1
    
      
  |