Step | Hyp | Ref
| Expression |
1 | | 2ndctop 20455 |
. 2

  |
2 | | is2ndc 20454 |
. . . 4

 
       |
3 | | ssrab2 3513 |
. . . . . . . . . . 11
   |
4 | | bastg 19974 |
. . . . . . . . . . . 12
       |
5 | 4 | 3ad2ant1 1028 |
. . . . . . . . . . 11
       
      |
6 | 3, 5 | syl5ss 3442 |
. . . . . . . . . 10
       

       |
7 | | fvex 5873 |
. . . . . . . . . . 11
     |
8 | 7 | elpw2 4566 |
. . . . . . . . . 10
       

       |
9 | 6, 8 | sylibr 216 |
. . . . . . . . 9
       

        |
10 | | vex 3047 |
. . . . . . . . . . 11
 |
11 | | ssdomg 7612 |
. . . . . . . . . . 11
   
     |
12 | 10, 3, 11 | mp2 9 |
. . . . . . . . . 10
   |
13 | | simp2 1008 |
. . . . . . . . . 10
       
  |
14 | | domtr 7619 |
. . . . . . . . . 10
    
    |
15 | 12, 13, 14 | sylancr 668 |
. . . . . . . . 9
       

   |
16 | | eltg2b 19967 |
. . . . . . . . . . . 12
       
     |
17 | 16 | 3ad2ant1 1028 |
. . . . . . . . . . 11
       
      
     |
18 | | elequ1 1893 |
. . . . . . . . . . . . . . 15
 
   |
19 | 18 | anbi1d 710 |
. . . . . . . . . . . . . 14
         |
20 | 19 | rexbidv 2900 |
. . . . . . . . . . . . 13
  
        |
21 | 20 | rspccv 3146 |
. . . . . . . . . . . 12
 

         |
22 | | id 22 |
. . . . . . . . . . . . . . . . 17
 
     |
23 | 22 | adantrr 722 |
. . . . . . . . . . . . . . . 16
  
 

   |
24 | | elequ2 1900 |
. . . . . . . . . . . . . . . . 17
 
   |
25 | 24 | elrab 3195 |
. . . . . . . . . . . . . . . 16
  

   |
26 | 23, 25 | sylibr 216 |
. . . . . . . . . . . . . . 15
  
 
    |
27 | 26 | adantl 468 |
. . . . . . . . . . . . . 14
  
       
       |
28 | | simprr 765 |
. . . . . . . . . . . . . 14
  
       
       |
29 | | elequ2 1900 |
. . . . . . . . . . . . . . . 16
 
   |
30 | | sseq1 3452 |
. . . . . . . . . . . . . . . 16
 
   |
31 | 29, 30 | anbi12d 716 |
. . . . . . . . . . . . . . 15
  
      |
32 | 31 | rspcev 3149 |
. . . . . . . . . . . . . 14
    
 
       |
33 | 27, 28, 32 | syl2anc 666 |
. . . . . . . . . . . . 13
  
       
          |
34 | 33 | rexlimdvaa 2879 |
. . . . . . . . . . . 12
       
 
  
       |
35 | 21, 34 | syl9r 74 |
. . . . . . . . . . 11
       
 

      
     |
36 | 17, 35 | sylbid 219 |
. . . . . . . . . 10
       
         
     |
37 | 36 | ralrimiv 2799 |
. . . . . . . . 9
       
          
    |
38 | | breq1 4404 |
. . . . . . . . . . 11
   
     |
39 | | rexeq 2987 |
. . . . . . . . . . . . 13
    

 
       |
40 | 39 | imbi2d 318 |
. . . . . . . . . . . 12
      
  
         |
41 | 40 | ralbidv 2826 |
. . . . . . . . . . 11
    
      

         
        |
42 | 38, 41 | anbi12d 716 |
. . . . . . . . . 10
            

                       |
43 | 42 | rspcev 3149 |
. . . . . . . . 9
           
          
    
             

     |
44 | 9, 15, 37, 43 | syl12anc 1265 |
. . . . . . . 8
       
              

     |
45 | 44 | 3expia 1209 |
. . . . . . 7
  
                    

      |
46 | | unieq 4205 |
. . . . . . . . 9
    
        |
47 | 46 | eleq2d 2513 |
. . . . . . . 8
    
     
    |
48 | | pweq 3953 |
. . . . . . . . 9
    
        |
49 | | raleq 2986 |
. . . . . . . . . 10
    
 
      

 




     |
50 | 49 | anbi2d 709 |
. . . . . . . . 9
    
 
        
  
  


      |
51 | 48, 50 | rexeqbidv 3001 |
. . . . . . . 8
    
 
     
        
  
   



      |
52 | 47, 51 | imbi12d 322 |
. . . . . . 7
    
       
             

         



       |
53 | 45, 52 | syl5ibcom 224 |
. . . . . 6
  
    
     



       |
54 | 53 | expimpd 607 |
. . . . 5
       
     



       |
55 | 54 | rexlimiv 2872 |
. . . 4
       
     



      |
56 | 2, 55 | sylbi 199 |
. . 3

  
   
 
      |
57 | 56 | ralrimiv 2799 |
. 2

      



     |
58 | | eqid 2450 |
. . 3
   |
59 | 58 | is1stc2 20450 |
. 2


      



      |
60 | 1, 57, 59 | sylanbrc 669 |
1

  |