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

      |
2 | | alexsub.3 |
. . . . . . . . . . . . . . . . . . . 20
           |
3 | 2 | eleq2d 2534 |
. . . . . . . . . . . . . . . . . . 19
             |
4 | 3 | anbi1d 719 |
. . . . . . . . . . . . . . . . . 18
   
        
    |
5 | 4 | biimpa 492 |
. . . . . . . . . . . . . . . . 17
 

          
   |
6 | 5 | adantlr 729 |
. . . . . . . . . . . . . . . 16
   
                
   |
7 | | tg2 20057 |
. . . . . . . . . . . . . . . 16
                     |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . 15
   
        
         |
9 | | alexsub.5 |
. . . . . . . . . . . . . . . . . 18
       |
10 | | ufilfil 20997 |
. . . . . . . . . . . . . . . . . 18
    
      |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
12 | 11 | ad3antrrr 744 |
. . . . . . . . . . . . . . . 16
    
 
   
 
    

         |
13 | | alexsub.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    |
14 | 9 | elfvexd 5907 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
15 | 13, 14 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
16 | | uniexb 6620 |
. . . . . . . . . . . . . . . . . . . . . . 23

   |
17 | 15, 16 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
18 | | elfi2 7946 |
. . . . . . . . . . . . . . . . . . . . . 22
     
             |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
      
            |
20 | 19 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 

                       |
21 | 11 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
            
  
      |
22 | | simplrr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
                 
     |
23 | | intss1 4241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    |
24 | 23 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           
    |
25 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           
    |
26 | 24, 25 | sseldd 3419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           
   |
27 | 26 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
 
             
 
   |
28 | | eldifsn 4088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       
       |
29 | 28 | simplbi 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
             |
30 | 29 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   
            
  
     |
31 | | elfpw 7894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   
    |
32 | 31 | simplbi 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      |
33 | 30, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
            
  
  |
34 | 33 | sselda 3418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
 
             
   |
35 | 34 | anasss 659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
                    |
36 | 35 | anim1i 578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
 
             
 
 
   |
37 | | eldif 3400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  

   |
38 | 36, 37 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
 
             
 
     |
39 | | elunii 4195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
  
     |
40 | 27, 38, 39 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
 
             
 
      |
41 | 40 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
                  
      |
42 | 22, 41 | mt3d 130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                    |
43 | 42 | expr 626 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
            
  

   |
44 | 43 | ssrdv 3424 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
            
  
  |
45 | 28 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          |
46 | 45 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
            
  
  |
47 | 31 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      |
48 | 30, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
            
  
  |
49 | | elfir 7947 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
  
      |
50 | 21, 44, 46, 48, 49 | syl13anc 1294 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
            
  
       |
51 | | filfi 20952 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
      |
52 | 21, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
            
  
      |
53 | 50, 52 | eleqtrd 2551 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
            
  
   |
54 | 53 | expr 626 |
. . . . . . . . . . . . . . . . . . . . . 22
   
                   |
55 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
56 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
57 | 55, 56 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . . . 22
   

       |
58 | 54, 57 | syl5ibrcom 230 |
. . . . . . . . . . . . . . . . . . . . 21
   
               
    |
59 | 58 | rexlimdva 2871 |
. . . . . . . . . . . . . . . . . . . 20
 

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

         

    |
61 | 60 | imp32 440 |
. . . . . . . . . . . . . . . . . 18
   
              |
62 | 61 | adantrrr 739 |
. . . . . . . . . . . . . . . . 17
   
             
  |
63 | 62 | adantlr 729 |
. . . . . . . . . . . . . . . 16
    
 
   
 
    

     |
64 | | elssuni 4219 |
. . . . . . . . . . . . . . . . . . 19
    |
65 | 64 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . 18
   
       
   |
66 | | fibas 20070 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
67 | | tgtopon 20064 |
. . . . . . . . . . . . . . . . . . . . . . 23
             TopOn         |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
        TopOn        |
69 | 2, 68 | syl6eqel 2557 |
. . . . . . . . . . . . . . . . . . . . 21
 TopOn         |
70 | | fiuni 7960 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
71 | 17, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
72 | 13, 71 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . 22
        |
73 | 72 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
 TopOn  TopOn         |
74 | 69, 73 | eleqtrrd 2552 |
. . . . . . . . . . . . . . . . . . . 20
 TopOn    |
75 | | toponuni 20019 |
. . . . . . . . . . . . . . . . . . . 20
 TopOn 
   |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    |
77 | 76 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
   
       
   |
78 | 65, 77 | sseqtr4d 3455 |
. . . . . . . . . . . . . . . . 17
   
       
  |
79 | 78 | adantr 472 |
. . . . . . . . . . . . . . . 16
    
 
   
 
    

     |
80 | | simprrr 783 |
. . . . . . . . . . . . . . . 16
    
 
   
 
    

     |
81 | | filss 20946 |
. . . . . . . . . . . . . . . 16
           |
82 | 12, 63, 79, 80, 81 | syl13anc 1294 |
. . . . . . . . . . . . . . 15
    
 
   
 
    

     |
83 | 8, 82 | rexlimddv 2875 |
. . . . . . . . . . . . . 14
   
          |
84 | 83 | expr 626 |
. . . . . . . . . . . . 13
   
          |
85 | 84 | ralrimiva 2809 |
. . . . . . . . . . . 12
 

      
   |
86 | 85 | expr 626 |
. . . . . . . . . . 11
 
 
   

    |
87 | 86 | imdistanda 707 |
. . . . . . . . . 10
         
     |
88 | 1, 87 | syl5bi 225 |
. . . . . . . . 9
        

     |
89 | | flimopn 21068 |
. . . . . . . . . 10
  TopOn         



     |
90 | 74, 11, 89 | syl2anc 673 |
. . . . . . . . 9
  
         |
91 | 88, 90 | sylibrd 242 |
. . . . . . . 8
       
    |
92 | 91 | ssrdv 3424 |
. . . . . . 7
   
 
    |
93 | | alexsub.6 |
. . . . . . 7
     |
94 | | sseq0 3769 |
. . . . . . 7
    
 
    
       |
95 | 92, 93, 94 | syl2anc 673 |
. . . . . 6
   
    |
96 | | ssdif0 3741 |
. . . . . 6
   
       |
97 | 95, 96 | sylibr 217 |
. . . . 5

     |
98 | | difss 3549 |
. . . . . . 7
   |
99 | 98 | unissi 4213 |
. . . . . 6
     |
100 | 99, 13 | syl5sseqr 3467 |
. . . . 5
      |
101 | 97, 100 | eqssd 3435 |
. . . 4
      |
102 | 101, 98 | jctil 546 |
. . 3
   
 
    |
103 | | difexg 4545 |
. . . . . 6
     |
104 | 17, 103 | syl 17 |
. . . . 5
     |
105 | 104 | adantr 472 |
. . . 4
 
    
       |
106 | | sseq1 3439 |
. . . . . . . 8
   
     |
107 | | unieq 4198 |
. . . . . . . . 9
         |
108 | 107 | eqeq2d 2481 |
. . . . . . . 8
   
       |
109 | 106, 108 | anbi12d 725 |
. . . . . . 7
    
 
    
     |
110 | 109 | anbi2d 718 |
. . . . . 6
    

  
   
 
      |
111 | | pweq 3945 |
. . . . . . . 8
   
     |
112 | 111 | ineq1d 3624 |
. . . . . . 7
    
        |
113 | 112 | rexeqdv 2980 |
. . . . . 6
    
 
 
     
 
    |
114 | 110, 113 | imbi12d 327 |
. . . . 5
      
         
      
               |
115 | | alexsub.4 |
. . . . 5
 
        
   |
116 | 114, 115 | vtoclg 3093 |
. . . 4
    
  
    
           |
117 | 105, 116 | mpcom 36 |
. . 3
 
    
             |
118 | 102, 117 | mpdan 681 |
. 2
       
   |
119 | | unieq 4198 |
. . . . . . 7

    |
120 | | uni0 4217 |
. . . . . . 7
  |
121 | 119, 120 | syl6eq 2521 |
. . . . . 6

   |
122 | 121 | neeq2d 2703 |
. . . . 5

 
   |
123 | | difssd 3550 |
. . . . . . . . . . 11
 
          |
124 | 123 | ralrimivw 2810 |
. . . . . . . . . 10
 
      
    |
125 | | riinn0 4344 |
. . . . . . . . . 10
    
      
    |
126 | 124, 125 | sylan 479 |
. . . . . . . . 9
               
    |
127 | 14 | ad2antrr 740 |
. . . . . . . . . . . . 13
            |
128 | | difexg 4545 |
. . . . . . . . . . . . 13
     |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . 12
              |
130 | 129 | ralrimivw 2810 |
. . . . . . . . . . 11
          
    |
131 | | dfiin2g 4302 |
. . . . . . . . . . 11
 
             |
132 | 130, 131 | syl 17 |
. . . . . . . . . 10
          
    

    |
133 | | eqid 2471 |
. . . . . . . . . . . 12
         |
134 | 133 | rnmpt 5086 |
. . . . . . . . . . 11
          |
135 | 134 | inteqi 4230 |
. . . . . . . . . 10
       

   |
136 | 132, 135 | syl6eqr 2523 |
. . . . . . . . 9
          
         |
137 | 126, 136 | eqtrd 2505 |
. . . . . . . 8
                      |
138 | 11 | ad2antrr 740 |
. . . . . . . . 9
                |
139 | | elfpw 7894 |
. . . . . . . . . . . . . . . 16
     
  
   |
140 | 139 | simplbi 467 |
. . . . . . . . . . . . . . 15
          |
141 | 140 | ad2antlr 741 |
. . . . . . . . . . . . . 14
              |
142 | 141 | sselda 3418 |
. . . . . . . . . . . . 13
   
  
   
     |
143 | 142 | eldifbd 3403 |
. . . . . . . . . . . 12
   
  
   
   |
144 | 9 | ad3antrrr 744 |
. . . . . . . . . . . . 13
   
  
   
       |
145 | 141 | difss2d 3552 |
. . . . . . . . . . . . . . . 16
            |
146 | 145 | sselda 3418 |
. . . . . . . . . . . . . . 15
   
  
   
   |
147 | | elssuni 4219 |
. . . . . . . . . . . . . . 15
    |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . 14
   
  
   

   |
149 | 13 | ad3antrrr 744 |
. . . . . . . . . . . . . 14
   
  
   
    |
150 | 148, 149 | sseqtr4d 3455 |
. . . . . . . . . . . . 13
   
  
   

  |
151 | | ufilb 20999 |
. . . . . . . . . . . . 13
       
     |
152 | 144, 150,
151 | syl2anc 673 |
. . . . . . . . . . . 12
   
  
   
       |
153 | 143, 152 | mpbid 215 |
. . . . . . . . . . 11
   
  
   
     |
154 | 153, 133 | fmptd 6061 |
. . . . . . . . . 10
                    |
155 | | frn 5747 |
. . . . . . . . . 10
        

     |
156 | 154, 155 | syl 17 |
. . . . . . . . 9
                |
157 | 133, 153 | dmmptd 5718 |
. . . . . . . . . . 11
                |
158 | | simpr 468 |
. . . . . . . . . . 11
            |
159 | 157, 158 | eqnetrd 2710 |
. . . . . . . . . 10
                |
160 | | dm0rn0 5057 |
. . . . . . . . . . 11
           |
161 | 160 | necon3bii 2695 |
. . . . . . . . . 10
    
      |
162 | 159, 161 | sylib 201 |
. . . . . . . . 9
                |
163 | 139 | simprbi 471 |
. . . . . . . . . . 11
        |
164 | 163 | ad2antlr 741 |
. . . . . . . . . 10
            |
165 | | abrexfi 7892 |
. . . . . . . . . . 11
        |
166 | 134, 165 | syl5eqel 2553 |
. . . . . . . . . 10
       |
167 | 164, 166 | syl 17 |
. . . . . . . . 9
                |
168 | | filintn0 20954 |
. . . . . . . . 9
                            |
169 | 138, 156,
162, 167, 168 | syl13anc 1294 |
. . . . . . . 8
                 |
170 | 137, 169 | eqnetrd 2710 |
. . . . . . 7
                 |
171 | | disj3 3813 |
. . . . . . . 8
  
          |
172 | 171 | necon3bii 2695 |
. . . . . . 7
  
          |
173 | 170, 172 | sylib 201 |
. . . . . 6
           
     |
174 | | iundif2 4336 |
. . . . . . 7

     
    |
175 | | dfss4 3668 |
. . . . . . . . . 10

      |
176 | 150, 175 | sylib 201 |
. . . . . . . . 9
   
  
   
       |
177 | 176 | iuneq2dv 4291 |
. . . . . . . 8
          
    
  |
178 | | uniiun 4322 |
. . . . . . . 8
   |
179 | 177, 178 | syl6eqr 2523 |
. . . . . . 7
          
       |
180 | 174, 179 | syl5eqr 2519 |
. . . . . 6
                  |
181 | 173, 180 | neeqtrd 2712 |
. . . . 5
             |
182 | 11 | adantr 472 |
. . . . . 6
 
            |
183 | | filtop 20948 |
. . . . . . 7
    
  |
184 | | fileln0 20943 |
. . . . . . 7
         |
185 | 183, 184 | mpdan 681 |
. . . . . 6
    
  |
186 | 182, 185 | syl 17 |
. . . . 5
 
        |
187 | 122, 181,
186 | pm2.61ne 2728 |
. . . 4
 
         |
188 | 187 | neneqd 2648 |
. . 3
 
     
   |
189 | 188 | nrexdv 2842 |
. 2
           |
190 | 118, 189 | pm2.65i 178 |
1
 |