Step | Hyp | Ref
| Expression |
1 | | simpr 468 |
. . . . . . . . 9
 
   |
2 | | neibastop1.4 |
. . . . . . . . . 10
 

         |
3 | | ssrab2 3500 |
. . . . . . . . . 10
  
          |
4 | 2, 3 | eqsstri 3448 |
. . . . . . . . 9
  |
5 | 1, 4 | syl6ss 3430 |
. . . . . . . 8
 
    |
6 | | sspwuni 4360 |
. . . . . . . 8
 
   |
7 | 5, 6 | sylib 201 |
. . . . . . 7
 
    |
8 | | vex 3034 |
. . . . . . . . 9
 |
9 | 8 | uniex 6606 |
. . . . . . . 8
  |
10 | 9 | elpw 3948 |
. . . . . . 7
 
 
  |
11 | 7, 10 | sylibr 217 |
. . . . . 6
 
     |
12 | | eluni2 4194 |
. . . . . . . 8
 

  |
13 | | elssuni 4219 |
. . . . . . . . . . . . 13
    |
14 | 13 | ad2antrl 742 |
. . . . . . . . . . . 12
    
 
   |
15 | | sspwb 4649 |
. . . . . . . . . . . 12
 
     |
16 | 14, 15 | sylib 201 |
. . . . . . . . . . 11
    
 
     |
17 | | sslin 3649 |
. . . . . . . . . . 11
 
             
     |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
    
 
                 |
19 | 1 | sselda 3418 |
. . . . . . . . . . . . 13
       |
20 | 19 | adantrr 731 |
. . . . . . . . . . . 12
    
 
  |
21 | | pweq 3945 |
. . . . . . . . . . . . . . . . 17
 
   |
22 | 21 | ineq2d 3625 |
. . . . . . . . . . . . . . . 16
     
           |
23 | 22 | neeq1d 2702 |
. . . . . . . . . . . . . . 15
        
          |
24 | 23 | raleqbi1dv 2981 |
. . . . . . . . . . . . . 14
  
      

          |
25 | 24, 2 | elrab2 3186 |
. . . . . . . . . . . . 13

  
    
     |
26 | 25 | simprbi 471 |
. . . . . . . . . . . 12
 
         |
27 | 20, 26 | syl 17 |
. . . . . . . . . . 11
    
 

         |
28 | | simprr 774 |
. . . . . . . . . . 11
    
 
  |
29 | | rsp 2773 |
. . . . . . . . . . 11
 
    
             |
30 | 27, 28, 29 | sylc 61 |
. . . . . . . . . 10
    
 
         |
31 | | ssn0 3770 |
. . . . . . . . . 10
             
  
       
          |
32 | 18, 30, 31 | syl2anc 673 |
. . . . . . . . 9
    
 
          |
33 | 32 | rexlimdvaa 2872 |
. . . . . . . 8
 
  
    
      |
34 | 12, 33 | syl5bi 225 |
. . . . . . 7
 
              |
35 | 34 | ralrimiv 2808 |
. . . . . 6
 
              |
36 | | pweq 3945 |
. . . . . . . . . 10
  
    |
37 | 36 | ineq2d 3625 |
. . . . . . . . 9
             
     |
38 | 37 | neeq1d 2702 |
. . . . . . . 8
                     |
39 | 38 | raleqbi1dv 2981 |
. . . . . . 7
                         |
40 | 39, 2 | elrab2 3186 |
. . . . . 6
 
 
               |
41 | 11, 35, 40 | sylanbrc 677 |
. . . . 5
 
    |
42 | 41 | ex 441 |
. . . 4
      |
43 | 42 | alrimiv 1781 |
. . 3
        |
44 | | pweq 3945 |
. . . . . . . . . . 11
 
   |
45 | 44 | ineq2d 3625 |
. . . . . . . . . 10
     
           |
46 | 45 | neeq1d 2702 |
. . . . . . . . 9
        
          |
47 | 46 | raleqbi1dv 2981 |
. . . . . . . 8
  
      

          |
48 | 47, 2 | elrab2 3186 |
. . . . . . 7

  
    
     |
49 | 48, 25 | anbi12i 711 |
. . . . . 6
 
            
              |
50 | | an4 840 |
. . . . . 6
            
                          
    
      |
51 | 49, 50 | bitri 257 |
. . . . 5
 
       
       
    
      |
52 | | inss1 3643 |
. . . . . . . . . 10
   |
53 | | elpwi 3951 |
. . . . . . . . . 10
 
  |
54 | 52, 53 | syl5ss 3429 |
. . . . . . . . 9
   
  |
55 | 54 | ad2antrl 742 |
. . . . . . . 8
 
         |
56 | 55 | adantrr 731 |
. . . . . . 7
 
  
   
       
    
    
    |
57 | 8 | inex1 4537 |
. . . . . . . 8
   |
58 | 57 | elpw 3948 |
. . . . . . 7
   
    |
59 | 56, 58 | sylibr 217 |
. . . . . 6
 
  
   
       
    
    
     |
60 | | ssralv 3479 |
. . . . . . . . . . 11
    
                     |
61 | 52, 60 | ax-mp 5 |
. . . . . . . . . 10
 
    
               |
62 | | inss2 3644 |
. . . . . . . . . . 11
   |
63 | | ssralv 3479 |
. . . . . . . . . . 11
    
                     |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . 10
 
    
               |
65 | 61, 64 | anim12i 576 |
. . . . . . . . 9
          
    
                             |
66 | | r19.26 2904 |
. . . . . . . . 9
 
        
      
  
 
                        |
67 | 65, 66 | sylibr 217 |
. . . . . . . 8
          
    
   

                    |
68 | | n0 3732 |
. . . . . . . . . . 11
     
 
          |
69 | | n0 3732 |
. . . . . . . . . . 11
     
 

         |
70 | 68, 69 | anbi12i 711 |
. . . . . . . . . 10
             
  
 
    
 

          |
71 | | eeanv 2093 |
. . . . . . . . . . 11
                 
  
 
    
 

          |
72 | | inss2 3644 |
. . . . . . . . . . . . . . . . . . 19
         |
73 | | simprl 772 |
. . . . . . . . . . . . . . . . . . 19
        
        
 
             
    |
74 | 72, 73 | sseldi 3416 |
. . . . . . . . . . . . . . . . . 18
        
        
 
            |
75 | 74 | elpwid 3952 |
. . . . . . . . . . . . . . . . 17
        
        
 
           |
76 | | inss2 3644 |
. . . . . . . . . . . . . . . . . . 19
         |
77 | | simprr 774 |
. . . . . . . . . . . . . . . . . . 19
        
        
 
             
    |
78 | 76, 77 | sseldi 3416 |
. . . . . . . . . . . . . . . . . 18
        
        
 
            |
79 | 78 | elpwid 3952 |
. . . . . . . . . . . . . . . . 17
        
        
 
           |
80 | | ss2in 3650 |
. . . . . . . . . . . . . . . . 17
 
  
    |
81 | 75, 79, 80 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
        
        
 
           
   |
82 | | sspwb 4649 |
. . . . . . . . . . . . . . . 16
    
 
      |
83 | 81, 82 | sylib 201 |
. . . . . . . . . . . . . . 15
        
        
 
                 |
84 | | sslin 3649 |
. . . . . . . . . . . . . . 15
   
 
              
 
    |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . 14
        
        
 
                             |
86 | | simplll 776 |
. . . . . . . . . . . . . . 15
        
        
 
           |
87 | 55 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
        
        
 
             |
88 | | simplr 770 |
. . . . . . . . . . . . . . . 16
        
        
 
             |
89 | 87, 88 | sseldd 3419 |
. . . . . . . . . . . . . . 15
        
        
 
           |
90 | | inss1 3643 |
. . . . . . . . . . . . . . . 16
            |
91 | 90, 73 | sseldi 3416 |
. . . . . . . . . . . . . . 15
        
        
 
               |
92 | | inss1 3643 |
. . . . . . . . . . . . . . . 16
            |
93 | 92, 77 | sseldi 3416 |
. . . . . . . . . . . . . . 15
        
        
 
               |
94 | | neibastop1.3 |
. . . . . . . . . . . . . . 15
 

   
          
 
    |
95 | 86, 89, 91, 93, 94 | syl13anc 1294 |
. . . . . . . . . . . . . 14
        
        
 
                    |
96 | | ssn0 3770 |
. . . . . . . . . . . . . 14
               
 
 
         
           |
97 | 85, 95, 96 | syl2anc 673 |
. . . . . . . . . . . . 13
        
        
 
                    |
98 | 97 | ex 441 |
. . . . . . . . . . . 12
    
  
                                |
99 | 98 | exlimdvv 1788 |
. . . . . . . . . . 11
    
  
                                    |
100 | 71, 99 | syl5bir 226 |
. . . . . . . . . 10
    
  
                                  |
101 | 70, 100 | syl5bi 225 |
. . . . . . . . 9
    
  
                        
 
     |
102 | 101 | ralimdva 2805 |
. . . . . . . 8
 
                                          |
103 | 67, 102 | syl5 32 |
. . . . . . 7
 
       
    
  
    
   

              |
104 | 103 | impr 631 |
. . . . . 6
 
  
   
       
    
    
               |
105 | | pweq 3945 |
. . . . . . . . . 10
   
 
   |
106 | 105 | ineq2d 3625 |
. . . . . . . . 9
       
             |
107 | 106 | neeq1d 2702 |
. . . . . . . 8
          
            |
108 | 107 | raleqbi1dv 2981 |
. . . . . . 7
    
      
                |
109 | 108, 2 | elrab2 3186 |
. . . . . 6
  
 
  
               |
110 | 59, 104, 109 | sylanbrc 677 |
. . . . 5
 
  
   
       
    
    
    |
111 | 51, 110 | sylan2b 483 |
. . . 4
 

      |
112 | 111 | ralrimivva 2814 |
. . 3
  
    |
113 | | neibastop1.1 |
. . . . . 6
   |
114 | | sspwuni 4360 |
. . . . . . . 8
 
   |
115 | 4, 114 | mpbi 213 |
. . . . . . 7
  |
116 | 115 | a1i 11 |
. . . . . 6
    |
117 | 113, 116 | ssexd 4543 |
. . . . 5
    |
118 | | uniexb 6620 |
. . . . 5

   |
119 | 117, 118 | sylibr 217 |
. . . 4
   |
120 | | istopg 20002 |
. . . 4
 
     


      |
121 | 119, 120 | syl 17 |
. . 3
       


      |
122 | 43, 112, 121 | mpbir2and 936 |
. 2
   |
123 | | pwidg 3955 |
. . . . . 6
    |
124 | 113, 123 | syl 17 |
. . . . 5
    |
125 | | neibastop1.2 |
. . . . . . . . . 10
             |
126 | 125 | ffvelrnda 6037 |
. . . . . . . . 9
 
             |
127 | | eldifi 3544 |
. . . . . . . . 9
                   |
128 | | elpwi 3951 |
. . . . . . . . 9
          
   |
129 | 126, 127,
128 | 3syl 18 |
. . . . . . . 8
 
        |
130 | | df-ss 3404 |
. . . . . . . 8
     
             |
131 | 129, 130 | sylib 201 |
. . . . . . 7
 
     
        |
132 | | eldifsni 4089 |
. . . . . . . 8
                 |
133 | 126, 132 | syl 17 |
. . . . . . 7
 
       |
134 | 131, 133 | eqnetrd 2710 |
. . . . . 6
 
     
    |
135 | 134 | ralrimiva 2809 |
. . . . 5
           |
136 | | pweq 3945 |
. . . . . . . . 9
 
   |
137 | 136 | ineq2d 3625 |
. . . . . . . 8
     
           |
138 | 137 | neeq1d 2702 |
. . . . . . 7
        
          |
139 | 138 | raleqbi1dv 2981 |
. . . . . 6
  
      

          |
140 | 139, 2 | elrab2 3186 |
. . . . 5

  
    
     |
141 | 124, 135,
140 | sylanbrc 677 |
. . . 4
   |
142 | | elssuni 4219 |
. . . 4
    |
143 | 141, 142 | syl 17 |
. . 3

   |
144 | 143, 116 | eqssd 3435 |
. 2
    |
145 | | istopon 20017 |
. 2
 TopOn  
    |
146 | 122, 144,
145 | sylanbrc 677 |
1
 TopOn    |