Step | Hyp | Ref
| Expression |
1 | | ssrab 3233 |
. . . . 5
   
     
    |
2 | | simprl 529 |
. . . . . . . . 9
  

  

  
   |
3 | | sspwuni 3971 |
. . . . . . . . 9
 
   |
4 | 2, 3 | sylib 122 |
. . . . . . . 8
  

  

  
   |
5 | | vuniex 4438 |
. . . . . . . . 9
  |
6 | 5 | elpw 3581 |
. . . . . . . 8
 
 
  |
7 | 4, 6 | sylibr 134 |
. . . . . . 7
  

  

  
    |
8 | | eluni2 3813 |
. . . . . . . . . 10
 

  |
9 | | r19.29 2614 |
. . . . . . . . . . . . 13
      

 

   |
10 | | simpr 110 |
. . . . . . . . . . . . . . . 16
  
 

   |
11 | 10 | impr 379 |
. . . . . . . . . . . . . . 15
   
  
  |
12 | | elssuni 3837 |
. . . . . . . . . . . . . . . 16
    |
13 | 12 | adantr 276 |
. . . . . . . . . . . . . . 15
   
      |
14 | 11, 13 | eqsstrrd 3192 |
. . . . . . . . . . . . . 14
   
      |
15 | 14 | rexlimiva 2589 |
. . . . . . . . . . . . 13
     
   |
16 | 9, 15 | syl 14 |
. . . . . . . . . . . 12
      
   |
17 | 16 | ex 115 |
. . . . . . . . . . 11
 

  
    |
18 | 17 | ad2antll 491 |
. . . . . . . . . 10
  

  

  
 
    |
19 | 8, 18 | biimtrid 152 |
. . . . . . . . 9
  

  

  
      |
20 | 19, 4 | jctild 316 |
. . . . . . . 8
  

  

  
   
     |
21 | | eqss 3170 |
. . . . . . . 8
 
      |
22 | 20, 21 | imbitrrdi 162 |
. . . . . . 7
  

  

  
      |
23 | | eleq2 2241 |
. . . . . . . . 9
       |
24 | | eqeq1 2184 |
. . . . . . . . 9
   
   |
25 | 23, 24 | imbi12d 234 |
. . . . . . . 8
   

       |
26 | 25 | elrab 2893 |
. . . . . . 7
 
  
     
      |
27 | 7, 22, 26 | sylanbrc 417 |
. . . . . 6
  

  

  
  

    |
28 | 27 | ex 115 |
. . . . 5
 
   


  
  
     |
29 | 1, 28 | biimtrid 152 |
. . . 4
 
    
     
     |
30 | 29 | alrimiv 1874 |
. . 3
 
      
     
     |
31 | | inss1 3355 |
. . . . . . . . 9
   |
32 | | simprll 537 |
. . . . . . . . . 10
  

                |
33 | 32 | elpwid 3586 |
. . . . . . . . 9
  

               |
34 | 31, 33 | sstrid 3166 |
. . . . . . . 8
  

                 |
35 | | vex 2740 |
. . . . . . . . . 10
 |
36 | 35 | inex1 4137 |
. . . . . . . . 9
   |
37 | 36 | elpw 3581 |
. . . . . . . 8
   
    |
38 | 34, 37 | sylibr 134 |
. . . . . . 7
  

                  |
39 | | elin 3318 |
. . . . . . . 8
  

   |
40 | | simprlr 538 |
. . . . . . . . . 10
  

             
   |
41 | | simprrr 540 |
. . . . . . . . . 10
  

             
   |
42 | 40, 41 | anim12d 335 |
. . . . . . . . 9
  

                
    |
43 | | ineq12 3331 |
. . . . . . . . . 10
 
       |
44 | | inidm 3344 |
. . . . . . . . . 10
   |
45 | 43, 44 | eqtrdi 2226 |
. . . . . . . . 9
 
     |
46 | 42, 45 | syl6 33 |
. . . . . . . 8
  

                
    |
47 | 39, 46 | biimtrid 152 |
. . . . . . 7
  

               
     |
48 | 38, 47 | jca 306 |
. . . . . 6
  

                 
  
     |
49 | 48 | ex 115 |
. . . . 5
 
     
    
                 |
50 | | eleq2 2241 |
. . . . . . . 8
 
   |
51 | | eqeq1 2184 |
. . . . . . . 8
 
   |
52 | 50, 51 | imbi12d 234 |
. . . . . . 7
         |
53 | 52 | elrab 2893 |
. . . . . 6
   
    
    |
54 | | eleq2 2241 |
. . . . . . . 8
 
   |
55 | | eqeq1 2184 |
. . . . . . . 8
 
   |
56 | 54, 55 | imbi12d 234 |
. . . . . . 7
         |
57 | 56 | elrab 2893 |
. . . . . 6
   
    
    |
58 | 53, 57 | anbi12i 460 |
. . . . 5
    
    
      
    
     |
59 | | eleq2 2241 |
. . . . . . 7
   
     |
60 | | eqeq1 2184 |
. . . . . . 7
   
     |
61 | 59, 60 | imbi12d 234 |
. . . . . 6
               |
62 | 61 | elrab 2893 |
. . . . 5
     
        
      |
63 | 49, 58, 62 | 3imtr4g 205 |
. . . 4
 
    

 
  
   
  

     |
64 | 63 | ralrimivv 2558 |
. . 3
 
    
   
  
      
    |
65 | | pwexg 4180 |
. . . . . 6
 
  |
66 | 65 | adantr 276 |
. . . . 5
 
    |
67 | | rabexg 4146 |
. . . . 5
    
    |
68 | 66, 67 | syl 14 |
. . . 4
 
  

    |
69 | | istopg 13469 |
. . . 4
   
     
 
      
     
   
  
      
  
  

      |
70 | 68, 69 | syl 14 |
. . 3
 
    
 
      
     
   
  
      
  
  

      |
71 | 30, 64, 70 | mpbir2and 944 |
. 2
 
  

    |
72 | | pwidg 3589 |
. . . . . 6
    |
73 | 72 | adantr 276 |
. . . . 5
 
    |
74 | | eqidd 2178 |
. . . . . 6
 
   |
75 | 74 | a1d 22 |
. . . . 5
 
     |
76 | | eleq2 2241 |
. . . . . . 7
 
   |
77 | | eqeq1 2184 |
. . . . . . 7
 
   |
78 | 76, 77 | imbi12d 234 |
. . . . . 6
         |
79 | 78 | elrab 2893 |
. . . . 5
   
    
    |
80 | 73, 75, 79 | sylanbrc 417 |
. . . 4
 
   
    |
81 | | elssuni 3837 |
. . . 4
   
     
    |
82 | 80, 81 | syl 14 |
. . 3
 

   
    |
83 | | ssrab2 3240 |
. . . . 5
  
    |
84 | | sspwuni 3971 |
. . . . 5
   
  
   
    |
85 | 83, 84 | mpbi 145 |
. . . 4
   
   |
86 | 85 | a1i 9 |
. . 3
 
    
    |
87 | 82, 86 | eqssd 3172 |
. 2
 
    
    |
88 | | istopon 13483 |
. 2
   
  TopOn 
   
   


     |
89 | 71, 87, 88 | sylanbrc 417 |
1
 
  

  TopOn    |