Step | Hyp | Ref
| Expression |
1 | | ptcls.a |
. . . . 5
   |
2 | | ptcls.j |
. . . . . 6
 
 TopOn    |
3 | | topontop 19990 |
. . . . . 6
 TopOn 
  |
4 | 2, 3 | syl 17 |
. . . . 5
 
   |
5 | | ptcls.c |
. . . . . . 7
 
   |
6 | | toponuni 19991 |
. . . . . . . 8
 TopOn 
   |
7 | 2, 6 | syl 17 |
. . . . . . 7
 
    |
8 | 5, 7 | sseqtrd 3480 |
. . . . . 6
 
    |
9 | | eqid 2462 |
. . . . . . 7
   |
10 | 9 | clscld 20111 |
. . . . . 6
                  |
11 | 4, 8, 10 | syl2anc 671 |
. . . . 5
 
               |
12 | 1, 4, 11 | ptcldmpt 20678 |
. . . 4
                      |
13 | | ptcls.2 |
. . . . 5
       |
14 | 13 | fveq2i 5891 |
. . . 4
               |
15 | 12, 14 | syl6eleqr 2551 |
. . 3
                |
16 | 9 | sscls 20120 |
. . . . . 6
              |
17 | 4, 8, 16 | syl2anc 671 |
. . . . 5
 
           |
18 | 17 | ralrimiva 2814 |
. . . 4
            |
19 | | ss2ixp 7561 |
. . . 4
 
                    |
20 | 18, 19 | syl 17 |
. . 3
             |
21 | | eqid 2462 |
. . . 4
   |
22 | 21 | clsss2 20137 |
. . 3
              
 
                             |
23 | 15, 20, 22 | syl2anc 671 |
. 2
                     |
24 | | vex 3060 |
. . . . . . . 8
 |
25 | | eqeq1 2466 |
. . . . . . . . . 10
  
   
        |
26 | 25 | anbi2d 715 |
. . . . . . . . 9
    
         
                
     
              
               
        |
27 | 26 | exbidv 1779 |
. . . . . . . 8
      
          
               
     
    
         
                
         |
28 | 24, 27 | elab 3197 |
. . . . . . 7
                  
               
     
    
         
                
        |
29 | | nffvmpt1 5896 |
. . . . . . . . . . . . . . . . . 18
         |
30 | 29 | nfel2 2619 |
. . . . . . . . . . . . . . . . 17
             |
31 | | nfv 1772 |
. . . . . . . . . . . . . . . . 17
             |
32 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . 18
           |
33 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . 18
               |
34 | 32, 33 | eleq12d 2534 |
. . . . . . . . . . . . . . . . 17
                         |
35 | 30, 31, 34 | cbvral 3027 |
. . . . . . . . . . . . . . . 16
 
         

            |
36 | | simpr 467 |
. . . . . . . . . . . . . . . . . . 19
 
   |
37 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . . 20
     |
38 | 37 | fvmpt2 5980 |
. . . . . . . . . . . . . . . . . . 19
 
TopOn           |
39 | 36, 2, 38 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
 
         |
40 | 39 | eleq2d 2525 |
. . . . . . . . . . . . . . . . 17
 
                   |
41 | 40 | ralbidva 2836 |
. . . . . . . . . . . . . . . 16
                     |
42 | 35, 41 | syl5bb 265 |
. . . . . . . . . . . . . . 15
                     |
43 | 42 | anbi2d 715 |
. . . . . . . . . . . . . 14
   
          


        |
44 | 43 | adantr 471 |
. . . . . . . . . . . . 13
 
         
                        |
45 | 44 | biimpa 491 |
. . . . . . . . . . . 12
            


                     |
46 | | ptclsg.1 |
. . . . . . . . . . . . . . . 16
 
AC   |
47 | 46 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
            
       
       
AC   |
48 | | simpll 765 |
. . . . . . . . . . . . . . . . . . 19
            
       
         |
49 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
50 | 49 | elixp 7555 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
51 | 50 | simprbi 470 |
. . . . . . . . . . . . . . . . . . . 20
                         |
52 | 51 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . 19
            
       
                      |
53 | 9 | clsndisj 20140 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
                                     |
54 | 53 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . 22
                                   
    |
55 | 54 | 3expia 1217 |
. . . . . . . . . . . . . . . . . . . . 21
                                    
     |
56 | 4, 8, 55 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . 20
 
                                 
     |
57 | 56 | ralimdva 2808 |
. . . . . . . . . . . . . . . . . . 19
                                   
     |
58 | 48, 52, 57 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
            
       
                           
    |
59 | | simprlr 778 |
. . . . . . . . . . . . . . . . . . 19
            
       
              |
60 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . 21
            
       
       
      |
61 | 32 | cbvixpv 7566 |
. . . . . . . . . . . . . . . . . . . . 21

    
     |
62 | 60, 61 | syl6eleq 2550 |
. . . . . . . . . . . . . . . . . . . 20
            
       
       
      |
63 | 49 | elixp 7555 |
. . . . . . . . . . . . . . . . . . . . 21
       
           |
64 | 63 | simprbi 470 |
. . . . . . . . . . . . . . . . . . . 20
     

          |
65 | 62, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
            
       
                  |
66 | | r19.26 2929 |
. . . . . . . . . . . . . . . . . . 19
 
                                |
67 | 59, 65, 66 | sylanbrc 675 |
. . . . . . . . . . . . . . . . . 18
            
       
                        |
68 | | ralim 2789 |
. . . . . . . . . . . . . . . . . 18
 
                                      
         |
69 | 58, 67, 68 | sylc 62 |
. . . . . . . . . . . . . . . . 17
            
       
                |
70 | | rabn0 3764 |
. . . . . . . . . . . . . . . . . . 19
  
       
         |
71 | | dfin5 3424 |
. . . . . . . . . . . . . . . . . . . . 21
 
        
        |
72 | | inss2 3665 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
73 | | ssiun2 4335 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
74 | 72, 73 | syl5ss 3455 |
. . . . . . . . . . . . . . . . . . . . . 22
     
    |
75 | | dfss1 3649 |
. . . . . . . . . . . . . . . . . . . . . 22
     
        
          |
76 | 74, 75 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . 21
  
               |
77 | 71, 76 | syl5eqr 2510 |
. . . . . . . . . . . . . . . . . . . 20
                  |
78 | 77 | neeq1d 2695 |
. . . . . . . . . . . . . . . . . . 19
   
    
           |
79 | 70, 78 | syl5bbr 267 |
. . . . . . . . . . . . . . . . . 18
  
                |
80 | 79 | ralbiia 2830 |
. . . . . . . . . . . . . . . . 17
 

                |
81 | 69, 80 | sylibr 217 |
. . . . . . . . . . . . . . . 16
            
       
        
         |
82 | | nfv 1772 |
. . . . . . . . . . . . . . . . 17
  
        |
83 | | nfiu1 4322 |
. . . . . . . . . . . . . . . . . 18
  
 |
84 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . 20
       |
85 | | nfcsb1v 3391 |
. . . . . . . . . . . . . . . . . . . 20
  
 ![]_ ]_](_urbrack.gif)  |
86 | 84, 85 | nfin 3651 |
. . . . . . . . . . . . . . . . . . 19
         ![]_ ]_](_urbrack.gif)   |
87 | 86 | nfel2 2619 |
. . . . . . . . . . . . . . . . . 18
        ![]_ ]_](_urbrack.gif)   |
88 | 83, 87 | nfrex 2862 |
. . . . . . . . . . . . . . . . 17
  
        ![]_ ]_](_urbrack.gif)   |
89 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . 20
           |
90 | | csbeq1a 3384 |
. . . . . . . . . . . . . . . . . . . 20
   ![]_ ]_](_urbrack.gif)   |
91 | 89, 90 | ineq12d 3647 |
. . . . . . . . . . . . . . . . . . 19
     
      
 ![]_ ]_](_urbrack.gif)    |
92 | 91 | eleq2d 2525 |
. . . . . . . . . . . . . . . . . 18
       
       ![]_ ]_](_urbrack.gif)     |
93 | 92 | rexbidv 2913 |
. . . . . . . . . . . . . . . . 17
  
       
        ![]_ ]_](_urbrack.gif)     |
94 | 82, 88, 93 | cbvral 3027 |
. . . . . . . . . . . . . . . 16
 

        
        ![]_ ]_](_urbrack.gif)    |
95 | 81, 94 | sylib 201 |
. . . . . . . . . . . . . . 15
            
       
        
        ![]_ ]_](_urbrack.gif)    |
96 | | eleq1 2528 |
. . . . . . . . . . . . . . . 16
             ![]_ ]_](_urbrack.gif) 
        
  ![]_ ]_](_urbrack.gif)     |
97 | 96 | acni3 8504 |
. . . . . . . . . . . . . . 15
  
AC 

        ![]_ ]_](_urbrack.gif)                       ![]_ ]_](_urbrack.gif)     |
98 | 47, 95, 97 | syl2anc 671 |
. . . . . . . . . . . . . 14
            
       
              
          
 ![]_ ]_](_urbrack.gif)     |
99 | | ffn 5751 |
. . . . . . . . . . . . . . . 16
     
  |
100 | | nfv 1772 |
. . . . . . . . . . . . . . . . . 18
             |
101 | 86 | nfel2 2619 |
. . . . . . . . . . . . . . . . . 18
             ![]_ ]_](_urbrack.gif)   |
102 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . 19
           |
103 | 102, 91 | eleq12d 2534 |
. . . . . . . . . . . . . . . . . 18
           
        
  ![]_ ]_](_urbrack.gif)     |
104 | 100, 101,
103 | cbvral 3027 |
. . . . . . . . . . . . . . . . 17
 
                      ![]_ ]_](_urbrack.gif)    |
105 | | ne0i 3749 |
. . . . . . . . . . . . . . . . . 18
       
         |
106 | | vex 3060 |
. . . . . . . . . . . . . . . . . . 19
 |
107 | 106 | elixp 7555 |
. . . . . . . . . . . . . . . . . 18
         
        
    |
108 | | ixpin 7573 |
. . . . . . . . . . . . . . . . . . . 20

           
   |
109 | 61 | ineq1i 3642 |
. . . . . . . . . . . . . . . . . . . 20
 
           
   |
110 | 108, 109 | eqtr4i 2487 |
. . . . . . . . . . . . . . . . . . 19

           
   |
111 | 110 | neeq1i 2700 |
. . . . . . . . . . . . . . . . . 18
 
    
  
    
   |
112 | 105, 107,
111 | 3imtr3i 273 |
. . . . . . . . . . . . . . . . 17
                   
    |
113 | 104, 112 | sylan2br 483 |
. . . . . . . . . . . . . . . 16
            
 ![]_ ]_](_urbrack.gif)        
    |
114 | 99, 113 | sylan 478 |
. . . . . . . . . . . . . . 15
      
          
 ![]_ ]_](_urbrack.gif)        
    |
115 | 114 | exlimiv 1787 |
. . . . . . . . . . . . . 14
                  
  ![]_ ]_](_urbrack.gif)    
    
   |
116 | 98, 115 | syl 17 |
. . . . . . . . . . . . 13
            
       
        
    
   |
117 | 116 | expr 624 |
. . . . . . . . . . . 12
            


       
               |
118 | 45, 117 | syldan 477 |
. . . . . . . . . . 11
            


             
          
    |
119 | 118 | 3adantr3 1175 |
. . . . . . . . . 10
            


         
                   
   
 
         |
120 | | eleq2 2529 |
. . . . . . . . . . 11
     


       |
121 | | ineq1 3639 |
. . . . . . . . . . . 12
     
        
    |
122 | 121 | neeq1d 2695 |
. . . . . . . . . . 11
     
 
        
    |
123 | 120, 122 | imbi12d 326 |
. . . . . . . . . 10
     
   
 
     
 
          |
124 | 119, 123 | syl5ibrcom 230 |
. . . . . . . . 9
            


         
                       

       |
125 | 124 | expimpd 612 |
. . . . . . . 8
 
         
                                       
     |
126 | 125 | exlimdv 1790 |
. . . . . . 7
 
         
     
          
               
        
     |
127 | 28, 126 | syl5bi 225 |
. . . . . 6
 
         
      
          
               
       
       |
128 | 127 | ralrimiv 2812 |
. . . . 5
 
         
      
          
               
         
    |
129 | 4, 37 | fmptd 6069 |
. . . . . . . . . 10
         |
130 | | ffn 5751 |
. . . . . . . . . 10
           |
131 | 129, 130 | syl 17 |
. . . . . . . . 9
     |
132 | | eqid 2462 |
. . . . . . . . . 10
                 
               
           
         
                
        |
133 | 132 | ptval 20634 |
. . . . . . . . 9
    
                          
               
         |
134 | 1, 131, 133 | syl2anc 671 |
. . . . . . . 8
                           
               
         |
135 | 13, 134 | syl5eq 2508 |
. . . . . . 7
         
          
               
          |
136 | 135 | adantr 471 |
. . . . . 6
 
         
                    
               
         |
137 | 2 | ralrimiva 2814 |
. . . . . . . . 9
 
TopOn    |
138 | 13 | pttopon 20660 |
. . . . . . . . 9
   TopOn  
TopOn     |
139 | 1, 137, 138 | syl2anc 671 |
. . . . . . . 8
 TopOn     |
140 | | toponuni 19991 |
. . . . . . . 8
 TopOn 
 
   |
141 | 139, 140 | syl 17 |
. . . . . . 7
 
   |
142 | 141 | adantr 471 |
. . . . . 6
 
         
    |
143 | 132 | ptbas 20643 |
. . . . . . . 8
        
                 
               
        |
144 | 1, 129, 143 | syl2anc 671 |
. . . . . . 7
      
          
               
         |
145 | 144 | adantr 471 |
. . . . . 6
 
         
                 
               
        |
146 | 5 | ralrimiva 2814 |
. . . . . . . 8
    |
147 | | ss2ixp 7561 |
. . . . . . . 8
 
 
  |
148 | 146, 147 | syl 17 |
. . . . . . 7
     |
149 | 148 | adantr 471 |
. . . . . 6
 
         
 
  |
150 | 9 | clsss3 20123 |
. . . . . . . . . . 11
           
   |
151 | 4, 8, 150 | syl2anc 671 |
. . . . . . . . . 10
 
            |
152 | 151, 7 | sseqtr4d 3481 |
. . . . . . . . 9
 
           |
153 | 152 | ralrimiva 2814 |
. . . . . . . 8
            |
154 | | ss2ixp 7561 |
. . . . . . . 8
 
       
        
   |
155 | 153, 154 | syl 17 |
. . . . . . 7
          
  |
156 | 155 | sselda 3444 |
. . . . . 6
 
         
   |
157 | 136, 142,
145, 149, 156 | elcls3 20148 |
. . . . 5
 
         
         
      
          
               
         
     |
158 | 128, 157 | mpbird 240 |
. . . 4
 
         
           |
159 | 158 | ex 440 |
. . 3
  
                    |
160 | 159 | ssrdv 3450 |
. 2
                     |
161 | 23, 160 | eqssd 3461 |
1
                     |