Step | Hyp | Ref
| Expression |
1 | | eldif 3416 |
. . . . . . . . . 10
     

      |
2 | | alexsub.3 |
. . . . . . . . . . . . . . . . . . . 20
           |
3 | 2 | eleq2d 2516 |
. . . . . . . . . . . . . . . . . . 19
             |
4 | 3 | anbi1d 712 |
. . . . . . . . . . . . . . . . . 18
   
        
    |
5 | 4 | biimpa 487 |
. . . . . . . . . . . . . . . . 17
 

          
   |
6 | 5 | adantlr 722 |
. . . . . . . . . . . . . . . 16
   
                
   |
7 | | tg2 19992 |
. . . . . . . . . . . . . . . 16
                     |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . 15
   
        
         |
9 | | alexsub.5 |
. . . . . . . . . . . . . . . . . 18
       |
10 | | ufilfil 20931 |
. . . . . . . . . . . . . . . . . 18
    
      |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
12 | 11 | ad3antrrr 737 |
. . . . . . . . . . . . . . . 16
    
 
   
 
    

         |
13 | | alexsub.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    |
14 | 9 | elfvexd 5898 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
15 | 13, 14 | eqeltrrd 2532 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
16 | | uniexb 6606 |
. . . . . . . . . . . . . . . . . . . . . . 23

   |
17 | 15, 16 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
18 | | elfi2 7933 |
. . . . . . . . . . . . . . . . . . . . . 22
     
             |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
      
            |
20 | 19 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 

                       |
21 | 11 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
            
  
      |
22 | | simplrr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
                 
     |
23 | | intss1 4252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    |
24 | 23 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           
    |
25 | | simplr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           
    |
26 | 24, 25 | sseldd 3435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           
   |
27 | 26 | ad2antlr 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
 
             
 
   |
28 | | eldifsn 4100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       
       |
29 | 28 | simplbi 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
             |
30 | 29 | ad2antrl 735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   
            
  
     |
31 | | elfpw 7881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   
    |
32 | 31 | simplbi 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      |
33 | 30, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
            
  
  |
34 | 33 | sselda 3434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
 
             
   |
35 | 34 | anasss 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
                    |
36 | 35 | anim1i 572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
 
             
 
 
   |
37 | | eldif 3416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  

   |
38 | 36, 37 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
 
             
 
     |
39 | | elunii 4206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
  
     |
40 | 27, 38, 39 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
 
             
 
      |
41 | 40 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
                  
      |
42 | 22, 41 | mt3d 129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                    |
43 | 42 | expr 620 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
            
  

   |
44 | 43 | ssrdv 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
            
  
  |
45 | 28 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          |
46 | 45 | ad2antrl 735 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
            
  
  |
47 | 31 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      |
48 | 30, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
            
  
  |
49 | | elfir 7934 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
  
      |
50 | 21, 44, 46, 48, 49 | syl13anc 1271 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
            
  
       |
51 | | filfi 20886 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
      |
52 | 21, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
            
  
      |
53 | 50, 52 | eleqtrd 2533 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
            
  
   |
54 | 53 | expr 620 |
. . . . . . . . . . . . . . . . . . . . . 22
   
                   |
55 | | eleq2 2520 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
56 | | eleq1 2519 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
57 | 55, 56 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . 22
   

       |
58 | 54, 57 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . . . . . . 21
   
               
    |
59 | 58 | rexlimdva 2881 |
. . . . . . . . . . . . . . . . . . . 20
 

                     |
60 | 20, 59 | sylbid 219 |
. . . . . . . . . . . . . . . . . . 19
 

         

    |
61 | 60 | imp32 435 |
. . . . . . . . . . . . . . . . . 18
   
              |
62 | 61 | adantrrr 732 |
. . . . . . . . . . . . . . . . 17
   
             
  |
63 | 62 | adantlr 722 |
. . . . . . . . . . . . . . . 16
    
 
   
 
    

     |
64 | | elssuni 4230 |
. . . . . . . . . . . . . . . . . . 19
    |
65 | 64 | ad2antrl 735 |
. . . . . . . . . . . . . . . . . 18
   
       
   |
66 | | fibas 20005 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
67 | | tgtopon 19999 |
. . . . . . . . . . . . . . . . . . . . . . 23
             TopOn         |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
        TopOn        |
69 | 2, 68 | syl6eqel 2539 |
. . . . . . . . . . . . . . . . . . . . 21
 TopOn         |
70 | | fiuni 7947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
71 | 17, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
72 | 13, 71 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . . . . 22
        |
73 | 72 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . 21
 TopOn  TopOn         |
74 | 69, 73 | eleqtrrd 2534 |
. . . . . . . . . . . . . . . . . . . 20
 TopOn    |
75 | | toponuni 19954 |
. . . . . . . . . . . . . . . . . . . 20
 TopOn 
   |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    |
77 | 76 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . 18
   
       
   |
78 | 65, 77 | sseqtr4d 3471 |
. . . . . . . . . . . . . . . . 17
   
       
  |
79 | 78 | adantr 467 |
. . . . . . . . . . . . . . . 16
    
 
   
 
    

     |
80 | | simprrr 776 |
. . . . . . . . . . . . . . . 16
    
 
   
 
    

     |
81 | | filss 20880 |
. . . . . . . . . . . . . . . 16
           |
82 | 12, 63, 79, 80, 81 | syl13anc 1271 |
. . . . . . . . . . . . . . 15
    
 
   
 
    

     |
83 | 8, 82 | rexlimddv 2885 |
. . . . . . . . . . . . . 14
   
          |
84 | 83 | expr 620 |
. . . . . . . . . . . . 13
   
          |
85 | 84 | ralrimiva 2804 |
. . . . . . . . . . . 12
 

      
   |
86 | 85 | expr 620 |
. . . . . . . . . . 11
 
 
   

    |
87 | 86 | imdistanda 700 |
. . . . . . . . . 10
         
     |
88 | 1, 87 | syl5bi 221 |
. . . . . . . . 9
        

     |
89 | | flimopn 21002 |
. . . . . . . . . 10
  TopOn         



     |
90 | 74, 11, 89 | syl2anc 667 |
. . . . . . . . 9
  
         |
91 | 88, 90 | sylibrd 238 |
. . . . . . . 8
       
    |
92 | 91 | ssrdv 3440 |
. . . . . . 7
   
 
    |
93 | | alexsub.6 |
. . . . . . 7
     |
94 | | sseq0 3768 |
. . . . . . 7
    
 
    
       |
95 | 92, 93, 94 | syl2anc 667 |
. . . . . 6
   
    |
96 | | ssdif0 3825 |
. . . . . 6
   
       |
97 | 95, 96 | sylibr 216 |
. . . . 5

     |
98 | | difss 3562 |
. . . . . . 7
   |
99 | 98 | unissi 4224 |
. . . . . 6
     |
100 | 99, 13 | syl5sseqr 3483 |
. . . . 5
      |
101 | 97, 100 | eqssd 3451 |
. . . 4
      |
102 | 101, 98 | jctil 540 |
. . 3
   
 
    |
103 | | difexg 4554 |
. . . . . 6
     |
104 | 17, 103 | syl 17 |
. . . . 5
     |
105 | 104 | adantr 467 |
. . . 4
 
    
       |
106 | | sseq1 3455 |
. . . . . . . 8
   
     |
107 | | unieq 4209 |
. . . . . . . . 9
         |
108 | 107 | eqeq2d 2463 |
. . . . . . . 8
   
       |
109 | 106, 108 | anbi12d 718 |
. . . . . . 7
    
 
    
     |
110 | 109 | anbi2d 711 |
. . . . . 6
    

  
   
 
      |
111 | | pweq 3956 |
. . . . . . . 8
   
     |
112 | 111 | ineq1d 3635 |
. . . . . . 7
    
        |
113 | 112 | rexeqdv 2996 |
. . . . . 6
    
 
 
     
 
    |
114 | 110, 113 | imbi12d 322 |
. . . . 5
      
         
      
               |
115 | | alexsub.4 |
. . . . 5
 
        
   |
116 | 114, 115 | vtoclg 3109 |
. . . 4
    
  
    
           |
117 | 105, 116 | mpcom 37 |
. . 3
 
    
             |
118 | 102, 117 | mpdan 675 |
. 2
       
   |
119 | | unieq 4209 |
. . . . . . 7

    |
120 | | uni0 4228 |
. . . . . . 7
  |
121 | 119, 120 | syl6eq 2503 |
. . . . . 6

   |
122 | 121 | neeq2d 2686 |
. . . . 5

 
   |
123 | | difssd 3563 |
. . . . . . . . . . 11
 
          |
124 | 123 | ralrimivw 2805 |
. . . . . . . . . 10
 
      
    |
125 | | riinn0 4356 |
. . . . . . . . . 10
    
      
    |
126 | 124, 125 | sylan 474 |
. . . . . . . . 9
               
    |
127 | 14 | ad2antrr 733 |
. . . . . . . . . . . . 13
            |
128 | | difexg 4554 |
. . . . . . . . . . . . 13
     |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . 12
              |
130 | 129 | ralrimivw 2805 |
. . . . . . . . . . 11
          
    |
131 | | dfiin2g 4314 |
. . . . . . . . . . 11
 
             |
132 | 130, 131 | syl 17 |
. . . . . . . . . 10
          
    

    |
133 | | eqid 2453 |
. . . . . . . . . . . 12
         |
134 | 133 | rnmpt 5083 |
. . . . . . . . . . 11
          |
135 | 134 | inteqi 4241 |
. . . . . . . . . 10
       

   |
136 | 132, 135 | syl6eqr 2505 |
. . . . . . . . 9
          
         |
137 | 126, 136 | eqtrd 2487 |
. . . . . . . 8
                      |
138 | 11 | ad2antrr 733 |
. . . . . . . . 9
                |
139 | | elfpw 7881 |
. . . . . . . . . . . . . . . 16
     
  
   |
140 | 139 | simplbi 462 |
. . . . . . . . . . . . . . 15
          |
141 | 140 | ad2antlr 734 |
. . . . . . . . . . . . . 14
              |
142 | 141 | sselda 3434 |
. . . . . . . . . . . . 13
   
  
   
     |
143 | 142 | eldifbd 3419 |
. . . . . . . . . . . 12
   
  
   
   |
144 | 9 | ad3antrrr 737 |
. . . . . . . . . . . . 13
   
  
   
       |
145 | 141 | difss2d 3565 |
. . . . . . . . . . . . . . . 16
            |
146 | 145 | sselda 3434 |
. . . . . . . . . . . . . . 15
   
  
   
   |
147 | | elssuni 4230 |
. . . . . . . . . . . . . . 15
    |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . 14
   
  
   

   |
149 | 13 | ad3antrrr 737 |
. . . . . . . . . . . . . 14
   
  
   
    |
150 | 148, 149 | sseqtr4d 3471 |
. . . . . . . . . . . . 13
   
  
   

  |
151 | | ufilb 20933 |
. . . . . . . . . . . . 13
       
     |
152 | 144, 150,
151 | syl2anc 667 |
. . . . . . . . . . . 12
   
  
   
       |
153 | 143, 152 | mpbid 214 |
. . . . . . . . . . 11
   
  
   
     |
154 | 153, 133 | fmptd 6051 |
. . . . . . . . . 10
                    |
155 | | frn 5740 |
. . . . . . . . . 10
        

     |
156 | 154, 155 | syl 17 |
. . . . . . . . 9
                |
157 | 133, 153 | dmmptd 5713 |
. . . . . . . . . . 11
                |
158 | | simpr 463 |
. . . . . . . . . . 11
            |
159 | 157, 158 | eqnetrd 2693 |
. . . . . . . . . 10
                |
160 | | dm0rn0 5054 |
. . . . . . . . . . 11
           |
161 | 160 | necon3bii 2678 |
. . . . . . . . . 10
    
      |
162 | 159, 161 | sylib 200 |
. . . . . . . . 9
                |
163 | 139 | simprbi 466 |
. . . . . . . . . . 11
        |
164 | 163 | ad2antlr 734 |
. . . . . . . . . 10
            |
165 | | abrexfi 7879 |
. . . . . . . . . . 11
        |
166 | 134, 165 | syl5eqel 2535 |
. . . . . . . . . 10
       |
167 | 164, 166 | syl 17 |
. . . . . . . . 9
                |
168 | | filintn0 20888 |
. . . . . . . . 9
                            |
169 | 138, 156,
162, 167, 168 | syl13anc 1271 |
. . . . . . . 8
                 |
170 | 137, 169 | eqnetrd 2693 |
. . . . . . 7
                 |
171 | | disj3 3811 |
. . . . . . . 8
  
          |
172 | 171 | necon3bii 2678 |
. . . . . . 7
  
          |
173 | 170, 172 | sylib 200 |
. . . . . 6
           
     |
174 | | iundif2 4348 |
. . . . . . 7

     
    |
175 | | dfss4 3679 |
. . . . . . . . . 10

      |
176 | 150, 175 | sylib 200 |
. . . . . . . . 9
   
  
   
       |
177 | 176 | iuneq2dv 4303 |
. . . . . . . 8
          
    
  |
178 | | uniiun 4334 |
. . . . . . . 8
   |
179 | 177, 178 | syl6eqr 2505 |
. . . . . . 7
          
       |
180 | 174, 179 | syl5eqr 2501 |
. . . . . 6
                  |
181 | 173, 180 | neeqtrd 2695 |
. . . . 5
             |
182 | 11 | adantr 467 |
. . . . . 6
 
            |
183 | | filtop 20882 |
. . . . . . 7
    
  |
184 | | fileln0 20877 |
. . . . . . 7
         |
185 | 183, 184 | mpdan 675 |
. . . . . 6
    
  |
186 | 182, 185 | syl 17 |
. . . . 5
 
        |
187 | 122, 181,
186 | pm2.61ne 2711 |
. . . 4
 
         |
188 | 187 | neneqd 2631 |
. . 3
 
     
   |
189 | 188 | nrexdv 2845 |
. 2
           |
190 | 118, 189 | pm2.65i 177 |
1
 |