Step | Hyp | Ref
| Expression |
1 | | rabexg 4567 |
. . . . . . 7
       |
2 | 1 | ad2antrr 737 |
. . . . . 6
  

 
↾t         |
3 | | ssrab2 3526 |
. . . . . . 7
     |
4 | | elpwg 3971 |
. . . . . . 7
                  |
5 | 3, 4 | mpbiri 241 |
. . . . . 6
            |
6 | 2, 5 | syl 17 |
. . . . 5
  

 
↾t          |
7 | | unieq 4220 |
. . . . . . . 8
             |
8 | 7 | sseq2d 3472 |
. . . . . . 7
      
        |
9 | | pweq 3966 |
. . . . . . . . 9
     
       |
10 | 9 | ineq1d 3645 |
. . . . . . . 8
      
          |
11 | 10 | rexeqdv 3006 |
. . . . . . 7
      
 
  
             |
12 | 8, 11 | imbi12d 326 |
. . . . . 6
            
       
              |
13 | 12 | rspcva 3160 |
. . . . 5
          
                      
    |
14 | 6, 13 | sylan 478 |
. . . 4
   

 
↾t           
                      |
15 | 14 | ex 440 |
. . 3
  

 
↾t                                   |
16 | | cmpsub.1 |
. . . . . . . 8
  |
17 | 16 | restuni 20227 |
. . . . . . 7
  
  ↾t    |
18 | 17 | adantr 471 |
. . . . . 6
  

 
↾t  
  ↾t    |
19 | 18 | eqeq1d 2464 |
. . . . 5
  

 
↾t       ↾t      |
20 | | selpw 3970 |
. . . . . . . . . . 11
   ↾t   ↾t    |
21 | | eleq2 2529 |
. . . . . . . . . . . . . . 15
       |
22 | | eluni 4215 |
. . . . . . . . . . . . . . 15
 
  
   |
23 | 21, 22 | syl6bb 269 |
. . . . . . . . . . . . . 14
          |
24 | 23 | adantl 472 |
. . . . . . . . . . . . 13
   


↾t  
 

       |
25 | | ssel 3438 |
. . . . . . . . . . . . . . . . . . 19
  ↾t  

↾t     |
26 | 16 | sseq2i 3469 |
. . . . . . . . . . . . . . . . . . . . . . . 24

   |
27 | | uniexg 6615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    |
28 | | ssexg 4563 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
     |
29 | 28 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
    |
30 | 27, 29 | sylan 478 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      |
31 | 26, 30 | sylan2b 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
  |
32 | | elrest 15375 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   ↾t 


    |
33 | 31, 32 | syldan 477 |
. . . . . . . . . . . . . . . . . . . . . 22
     ↾t 


    |
34 | | inss1 3664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
35 | | sseq1 3465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
     |
36 | 34, 35 | mpbiri 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
37 | 36 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
   |
38 | 37 | 3ad2antl3 1178 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   

      |
39 | 38 | 3adant2 1033 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   

      |
40 | | simp12 1045 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   

      |
41 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
     |
42 | 41 | biimpa 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
     |
43 | 42 | 3ad2antl3 1178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   

    
   |
44 | 43 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   

    
   |
45 | | ineq1 3639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
     |
46 | 45 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
     |
47 | 46 | elrab 3208 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    


    |
48 | 40, 44, 47 | sylanbrc 675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   

          |
49 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
50 | | eleq2 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
51 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
       |
52 | 50, 51 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
53 | 49, 52 | spcev 3153 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 


             |
54 | 39, 48, 53 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

              |
55 | 54 | 3exp 1214 |
. . . . . . . . . . . . . . . . . . . . . . 23
  


 

             |
56 | 55 | rexlimdv3a 2893 |
. . . . . . . . . . . . . . . . . . . . . 22
       

             |
57 | 33, 56 | sylbid 223 |
. . . . . . . . . . . . . . . . . . . . 21
     ↾t                 |
58 | 57 | com23 81 |
. . . . . . . . . . . . . . . . . . . 20
     
↾t                |
59 | 58 | com4l 87 |
. . . . . . . . . . . . . . . . . . 19
   ↾t 

                |
60 | 25, 59 | sylcom 30 |
. . . . . . . . . . . . . . . . . 18
  ↾t  

                |
61 | 60 | com24 90 |
. . . . . . . . . . . . . . . . 17
  ↾t                    |
62 | 61 | impcom 436 |
. . . . . . . . . . . . . . . 16
  

 ↾t                 |
63 | 62 | impd 437 |
. . . . . . . . . . . . . . 15
  

 ↾t    

           |
64 | 63 | exlimdv 1790 |
. . . . . . . . . . . . . 14
  

 ↾t                   |
65 | 64 | adantr 471 |
. . . . . . . . . . . . 13
   


↾t  
 
                |
66 | 24, 65 | sylbid 223 |
. . . . . . . . . . . 12
   


↾t  
 

           |
67 | 66 | ex 440 |
. . . . . . . . . . 11
  

 ↾t   
              |
68 | 20, 67 | sylan2b 482 |
. . . . . . . . . 10
  

 
↾t     
            |
69 | 68 | imp 435 |
. . . . . . . . 9
   

 
↾t  
 

           |
70 | | eluni 4215 |
. . . . . . . . 9
     
          |
71 | 69, 70 | syl6ibr 235 |
. . . . . . . 8
   

 
↾t  
 

        |
72 | 71 | ssrdv 3450 |
. . . . . . 7
   

 
↾t  
 
       |
73 | | pm2.27 40 |
. . . . . . . . 9
                     
 
             |
74 | | elin 3629 |
. . . . . . . . . . 11
       
         |
75 | | vex 3060 |
. . . . . . . . . . . . . . . . . 18
 |
76 | | eqeq1 2466 |
. . . . . . . . . . . . . . . . . . 19
   
     |
77 | 76 | rexbidv 2913 |
. . . . . . . . . . . . . . . . . 18
  
 

     |
78 | 75, 77 | elab 3197 |
. . . . . . . . . . . . . . . . 17
      
    |
79 | | selpw 3970 |
. . . . . . . . . . . . . . . . . . . 20
     
      |
80 | | ssel 3438 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
81 | | ineq1 3639 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
     |
82 | 81 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
     |
83 | 82 | elrab 3208 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    


    |
84 | | eleq1a 2535 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
85 | 84 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
   |
86 | 83, 85 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
87 | 80, 86 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
88 | 87 | 2a1d 27 |
. . . . . . . . . . . . . . . . . . . . 21
           
  ↾t  
 

         |
89 | 88 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
 


         
  ↾t  
 

         |
90 | 79, 89 | sylanb 479 |
. . . . . . . . . . . . . . . . . . 19
         
   

 
↾t  
 

         |
91 | 90 | 3imp 1208 |
. . . . . . . . . . . . . . . . . 18
            

 
↾t  
           |
92 | 91 | rexlimdv 2889 |
. . . . . . . . . . . . . . . . 17
            

 
↾t  
    
     |
93 | 78, 92 | syl5bi 225 |
. . . . . . . . . . . . . . . 16
            

 
↾t  
            |
94 | 93 | ssrdv 3450 |
. . . . . . . . . . . . . . 15
            

 
↾t  
          |
95 | | vex 3060 |
. . . . . . . . . . . . . . . . 17
 |
96 | 95 | abrexex 6794 |
. . . . . . . . . . . . . . . 16
      |
97 | 96 | elpw 3969 |
. . . . . . . . . . . . . . 15
  
     
     |
98 | 94, 97 | sylibr 217 |
. . . . . . . . . . . . . 14
            

 
↾t  
           |
99 | | abrexfi 7900 |
. . . . . . . . . . . . . . . 16
        |
100 | 99 | ad2antlr 738 |
. . . . . . . . . . . . . . 15
           

     |
101 | 100 | 3adant3 1034 |
. . . . . . . . . . . . . 14
            

 
↾t  
          |
102 | 98, 101 | elind 3630 |
. . . . . . . . . . . . 13
            

 
↾t  
             |
103 | | dfss 3431 |
. . . . . . . . . . . . . . . . 17
 

    |
104 | 103 | biimpi 199 |
. . . . . . . . . . . . . . . 16
       |
105 | | uniiun 4345 |
. . . . . . . . . . . . . . . . . 18
   |
106 | 105 | ineq2i 3643 |
. . . . . . . . . . . . . . . . 17
       |
107 | | iunin2 4356 |
. . . . . . . . . . . . . . . . 17

   
  |
108 | | incom 3637 |
. . . . . . . . . . . . . . . . . . 19
     |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
       |
110 | 109 | iuneq2i 4311 |
. . . . . . . . . . . . . . . . 17

  

  |
111 | 106, 107,
110 | 3eqtr2i 2490 |
. . . . . . . . . . . . . . . 16
       |
112 | 104, 111 | syl6eq 2512 |
. . . . . . . . . . . . . . 15
       |
113 | 112 | 3ad2ant2 1036 |
. . . . . . . . . . . . . 14
            

 
↾t  
        |
114 | 18 | ad2antrl 739 |
. . . . . . . . . . . . . . 15
 
       ↾t       
↾t    |
115 | 114 | 3adant1 1032 |
. . . . . . . . . . . . . 14
            

 
↾t  
     ↾t    |
116 | | vex 3060 |
. . . . . . . . . . . . . . . . 17
 |
117 | 116 | inex1 4558 |
. . . . . . . . . . . . . . . 16
   |
118 | 117 | dfiun2 4326 |
. . . . . . . . . . . . . . 15

   

    |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . 14
            

 
↾t  
   
   

     |
120 | 113, 115,
119 | 3eqtr3d 2504 |
. . . . . . . . . . . . 13
            

 
↾t  
     ↾t   

     |
121 | | unieq 4220 |
. . . . . . . . . . . . . . 15
        

     |
122 | 121 | eqeq2d 2472 |
. . . . . . . . . . . . . 14
         ↾t     ↾t           |
123 | 122 | rspcev 3162 |
. . . . . . . . . . . . 13
   
        ↾t    
    
 
   
↾t     |
124 | 102, 120,
123 | syl2anc 671 |
. . . . . . . . . . . 12
            

 
↾t  
          ↾t     |
125 | 124 | 3exp 1214 |
. . . . . . . . . . 11
         
   

 
↾t  
 
       ↾t       |
126 | 74, 125 | sylbi 200 |
. . . . . . . . . 10
              
  ↾t  
 
       ↾t       |
127 | 126 | rexlimiv 2885 |
. . . . . . . . 9
               
  ↾t  
 
       ↾t      |
128 | 73, 127 | syl6 34 |
. . . . . . . 8
                     
 
   

 
↾t  
 
       ↾t       |
129 | 128 | com3r 82 |
. . . . . . 7
   

 
↾t  
 
                     
 
       ↾t       |
130 | 72, 129 | mpd 15 |
. . . . . 6
   

 
↾t  
 
                         ↾t      |
131 | 130 | ex 440 |
. . . . 5
  

 
↾t                      
       ↾t       |
132 | 19, 131 | sylbird 243 |
. . . 4
  

 
↾t      ↾t         
          
       ↾t       |
133 | 132 | com23 81 |
. . 3
  

 
↾t         
          
  
↾t          ↾t       |
134 | 15, 133 | syld 45 |
. 2
  

 
↾t                 
↾t          ↾t       |
135 | 134 | ralrimdva 2818 |
1
                 ↾t      ↾t          ↾t       |