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

  |
2 | | is2ndc 20538 |
. . . 4

 
       |
3 | | ssrab2 3500 |
. . . . . . . . . . 11
   |
4 | | bastg 20058 |
. . . . . . . . . . . 12
       |
5 | 4 | 3ad2ant1 1051 |
. . . . . . . . . . 11
       
      |
6 | 3, 5 | syl5ss 3429 |
. . . . . . . . . 10
       

       |
7 | | fvex 5889 |
. . . . . . . . . . 11
     |
8 | 7 | elpw2 4565 |
. . . . . . . . . 10
       

       |
9 | 6, 8 | sylibr 217 |
. . . . . . . . 9
       

        |
10 | | vex 3034 |
. . . . . . . . . . 11
 |
11 | | ssdomg 7633 |
. . . . . . . . . . 11
   
     |
12 | 10, 3, 11 | mp2 9 |
. . . . . . . . . 10
   |
13 | | simp2 1031 |
. . . . . . . . . 10
       
  |
14 | | domtr 7640 |
. . . . . . . . . 10
    
    |
15 | 12, 13, 14 | sylancr 676 |
. . . . . . . . 9
       

   |
16 | | eltg2b 20051 |
. . . . . . . . . . . 12
       
     |
17 | 16 | 3ad2ant1 1051 |
. . . . . . . . . . 11
       
      
     |
18 | | elequ1 1911 |
. . . . . . . . . . . . . . 15
 
   |
19 | 18 | anbi1d 719 |
. . . . . . . . . . . . . 14
         |
20 | 19 | rexbidv 2892 |
. . . . . . . . . . . . 13
  
        |
21 | 20 | rspccv 3133 |
. . . . . . . . . . . 12
 

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

   |
24 | | elequ2 1918 |
. . . . . . . . . . . . . . . . 17
 
   |
25 | 24 | elrab 3184 |
. . . . . . . . . . . . . . . 16
  

   |
26 | 23, 25 | sylibr 217 |
. . . . . . . . . . . . . . 15
  
 
    |
27 | 26 | adantl 473 |
. . . . . . . . . . . . . 14
  
       
       |
28 | | simprr 774 |
. . . . . . . . . . . . . 14
  
       
       |
29 | | elequ2 1918 |
. . . . . . . . . . . . . . . 16
 
   |
30 | | sseq1 3439 |
. . . . . . . . . . . . . . . 16
 
   |
31 | 29, 30 | anbi12d 725 |
. . . . . . . . . . . . . . 15
  
      |
32 | 31 | rspcev 3136 |
. . . . . . . . . . . . . 14
    
 
       |
33 | 27, 28, 32 | syl2anc 673 |
. . . . . . . . . . . . 13
  
       
          |
34 | 33 | rexlimdvaa 2872 |
. . . . . . . . . . . 12
       
 
  
       |
35 | 21, 34 | syl9r 73 |
. . . . . . . . . . 11
       
 

      
     |
36 | 17, 35 | sylbid 223 |
. . . . . . . . . 10
       
         
     |
37 | 36 | ralrimiv 2808 |
. . . . . . . . 9
       
          
    |
38 | | breq1 4398 |
. . . . . . . . . . 11
   
     |
39 | | rexeq 2974 |
. . . . . . . . . . . . 13
    

 
       |
40 | 39 | imbi2d 323 |
. . . . . . . . . . . 12
      
  
         |
41 | 40 | ralbidv 2829 |
. . . . . . . . . . 11
    
      

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

                       |
43 | 42 | rspcev 3136 |
. . . . . . . . 9
           
          
    
             

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

     |
45 | 44 | 3expia 1233 |
. . . . . . 7
  
                    

      |
46 | | unieq 4198 |
. . . . . . . . 9
    
        |
47 | 46 | eleq2d 2534 |
. . . . . . . 8
    
     
    |
48 | | pweq 3945 |
. . . . . . . . 9
    
        |
49 | | raleq 2973 |
. . . . . . . . . 10
    
 
      

 




     |
50 | 49 | anbi2d 718 |
. . . . . . . . 9
    
 
        
  
  


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



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

         



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



       |
54 | 53 | expimpd 614 |
. . . . 5
       
     



       |
55 | 54 | rexlimiv 2867 |
. . . 4
       
     



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

  
   
 
      |
57 | 56 | ralrimiv 2808 |
. 2

      



     |
58 | | eqid 2471 |
. . 3
   |
59 | 58 | is1stc2 20534 |
. 2


      



      |
60 | 1, 57, 59 | sylanbrc 677 |
1

  |