Step | Hyp | Ref
| Expression |
1 | | n0 3597 |
. . . 4
    |
2 | | rabeq0 3609 |
. . . . . . . 8
          |
3 | | breq1 4175 |
. . . . . . . . . . . . . 14
   
     |
4 | 3 | notbid 286 |
. . . . . . . . . . . . 13
   
     |
5 | 4 | cbvralv 2892 |
. . . . . . . . . . . 12
 
 

    |
6 | | breq2 4176 |
. . . . . . . . . . . . . 14
   
     |
7 | 6 | notbid 286 |
. . . . . . . . . . . . 13
   
     |
8 | 7 | ralbidv 2686 |
. . . . . . . . . . . 12
  
 

     |
9 | 5, 8 | syl5bb 249 |
. . . . . . . . . . 11
  
 

     |
10 | 9 | rspcev 3012 |
. . . . . . . . . 10
      

    |
11 | 10 | ex 424 |
. . . . . . . . 9
  
  

     |
12 | 11 | ad2antll 710 |
. . . . . . . 8
  
Se  
   
  

     |
13 | 2, 12 | syl5bi 209 |
. . . . . . 7
  
Se  
   
  


     |
14 | | simprl 733 |
. . . . . . . . . . 11
  
Se  
    |
15 | | simplr 732 |
. . . . . . . . . . 11
  
Se  
  Se   |
16 | | sess2 4511 |
. . . . . . . . . . 11
  Se
Se    |
17 | 14, 15, 16 | sylc 58 |
. . . . . . . . . 10
  
Se  
  Se   |
18 | | simprr 734 |
. . . . . . . . . 10
  
Se  
    |
19 | | seex 4505 |
. . . . . . . . . 10
  Se  
     |
20 | 17, 18, 19 | syl2anc 643 |
. . . . . . . . 9
  
Se  
  
     |
21 | | wefr 4532 |
. . . . . . . . . 10
   |
22 | 21 | ad2antrr 707 |
. . . . . . . . 9
  
Se  
    |
23 | | ssrab2 3388 |
. . . . . . . . . 10

    |
24 | 23, 14 | syl5ss 3319 |
. . . . . . . . 9
  
Se  
  
     |
25 | | fri 4504 |
. . . . . . . . . 10
         
               

       |
26 | 25 | expr 599 |
. . . . . . . . 9
            
           

        |
27 | 20, 22, 24, 26 | syl21anc 1183 |
. . . . . . . 8
  
Se  
   
  
                |
28 | | breq1 4175 |
. . . . . . . . . 10
   
     |
29 | 28 | rexrab 3058 |
. . . . . . . . 9
  
    

    

   

        |
30 | | breq1 4175 |
. . . . . . . . . . . . 13
   
     |
31 | 30 | ralrab 3056 |
. . . . . . . . . . . 12
 

    

        |
32 | | weso 4533 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
33 | 32 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . . . 21
  
Se  
    |
34 | | soss 4481 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
35 | 14, 33, 34 | sylc 58 |
. . . . . . . . . . . . . . . . . . . 20
  
Se  
    |
36 | 35 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . 19
     Se    


  |
37 | | simpr 448 |
. . . . . . . . . . . . . . . . . . 19
     Se    


  |
38 | | simplr 732 |
. . . . . . . . . . . . . . . . . . 19
     Se    


  |
39 | 18 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . 19
     Se    


  |
40 | | sotr 4485 |
. . . . . . . . . . . . . . . . . . 19
  
        
     |
41 | 36, 37, 38, 39, 40 | syl13anc 1186 |
. . . . . . . . . . . . . . . . . 18
     Se    


            |
42 | 41 | ancomsd 441 |
. . . . . . . . . . . . . . . . 17
     Se    


            |
43 | 42 | expdimp 427 |
. . . . . . . . . . . . . . . 16
      Se    


           |
44 | 43 | an32s 780 |
. . . . . . . . . . . . . . 15
      Se    
    
  
     |
45 | 44 | con3d 127 |
. . . . . . . . . . . . . 14
      Se    
    
        |
46 | | idd 22 |
. . . . . . . . . . . . . 14
      Se    
    
        |
47 | 45, 46 | jad 156 |
. . . . . . . . . . . . 13
      Se    
    
      
     |
48 | 47 | ralimdva 2744 |
. . . . . . . . . . . 12
     Se    
     
      
     |
49 | 31, 48 | syl5bi 209 |
. . . . . . . . . . 11
     Se    
                  |
50 | 49 | expimpd 587 |
. . . . . . . . . 10
    Se                 

     |
51 | 50 | reximdva 2778 |
. . . . . . . . 9
  
Se  
   
          


     |
52 | 29, 51 | syl5bi 209 |
. . . . . . . 8
  
Se  
   

    

     

     |
53 | 27, 52 | syld 42 |
. . . . . . 7
  
Se  
   
  


     |
54 | 13, 53 | pm2.61dne 2644 |
. . . . . 6
  
Se  
  

    |
55 | 54 | expr 599 |
. . . . 5
  
Se 
 


     |
56 | 55 | exlimdv 1643 |
. . . 4
  
Se 
   

     |
57 | 1, 56 | syl5bi 209 |
. . 3
  
Se 
   
     |
58 | 57 | impr 603 |
. 2
  
Se  
   
    |
59 | | simprl 733 |
. . . 4
  
Se  
    |
60 | 32 | ad2antrr 707 |
. . . 4
  
Se  
    |
61 | 59, 60, 34 | sylc 58 |
. . 3
  
Se  
    |
62 | | somo 4497 |
. . 3
 
 
    |
63 | 61, 62 | syl 16 |
. 2
  
Se  
         |
64 | | reu5 2881 |
. 2
  
 
 

  
 
     |
65 | 58, 63, 64 | sylanbrc 646 |
1
  
Se  
        |