Step | Hyp | Ref
| Expression |
1 | | ssel 3426 |
. . . . . . . . 9

    |
2 | 1 | pm4.71rd 641 |
. . . . . . . 8


     |
3 | 2 | exbidv 1768 |
. . . . . . 7

         |
4 | | df-rex 2743 |
. . . . . . . 8
 
      |
5 | | renegcl 9937 |
. . . . . . . . 9
    |
6 | | infm3lem 10567 |
. . . . . . . . 9
     |
7 | | eleq1 2517 |
. . . . . . . . 9
  
    |
8 | 5, 6, 7 | rexxfr 4620 |
. . . . . . . 8
 
    |
9 | 4, 8 | bitr3i 255 |
. . . . . . 7
    
    |
10 | 3, 9 | syl6bb 265 |
. . . . . 6

       |
11 | | n0 3741 |
. . . . . 6
    |
12 | | rabn0 3752 |
. . . . . 6
        |
13 | 10, 11, 12 | 3bitr4g 292 |
. . . . 5

       |
14 | | ssel 3426 |
. . . . . . . . . . . 12

    |
15 | 14 | pm4.71rd 641 |
. . . . . . . . . . 11


     |
16 | 15 | imbi1d 319 |
. . . . . . . . . 10

  
 

    |
17 | | impexp 448 |
. . . . . . . . . 10
     

    |
18 | 16, 17 | syl6bb 265 |
. . . . . . . . 9

  


     |
19 | 18 | albidv 1767 |
. . . . . . . 8

   
          |
20 | | df-ral 2742 |
. . . . . . . 8
 
      |
21 | | renegcl 9937 |
. . . . . . . . . 10
    |
22 | | infm3lem 10567 |
. . . . . . . . . 10
     |
23 | | eleq1 2517 |
. . . . . . . . . . 11
  
    |
24 | | breq2 4406 |
. . . . . . . . . . 11
  
    |
25 | 23, 24 | imbi12d 322 |
. . . . . . . . . 10
   
  
     |
26 | 21, 22, 25 | ralxfr 4618 |
. . . . . . . . 9
 
 
  
    |
27 | | df-ral 2742 |
. . . . . . . . 9
 
 
   
    |
28 | 26, 27 | bitr3i 255 |
. . . . . . . 8
 
   
   
    |
29 | 19, 20, 28 | 3bitr4g 292 |
. . . . . . 7

 
  
     |
30 | 29 | rexbidv 2901 |
. . . . . 6

  
         |
31 | | renegcl 9937 |
. . . . . . . 8
    |
32 | | infm3lem 10567 |
. . . . . . . 8
     |
33 | | breq1 4405 |
. . . . . . . . . 10
  

     |
34 | 33 | imbi2d 318 |
. . . . . . . . 9
    
          |
35 | 34 | ralbidv 2827 |
. . . . . . . 8
   
 
  
        |
36 | 31, 32, 35 | rexxfr 4620 |
. . . . . . 7
  
   
   
     |
37 | | negeq 9867 |
. . . . . . . . . . . . . . 15
     |
38 | 37 | eleq1d 2513 |
. . . . . . . . . . . . . 14
  
    |
39 | 38 | elrab 3196 |
. . . . . . . . . . . . 13
   
     |
40 | 39 | imbi1i 327 |
. . . . . . . . . . . 12
     
       |
41 | | impexp 448 |
. . . . . . . . . . . 12
   

 
 
    |
42 | 40, 41 | bitri 253 |
. . . . . . . . . . 11
     

 
    |
43 | 42 | albii 1691 |
. . . . . . . . . 10
            
    |
44 | | df-ral 2742 |
. . . . . . . . . 10
 
             |
45 | | df-ral 2742 |
. . . . . . . . . 10
 
 
   
 
    |
46 | 43, 44, 45 | 3bitr4ri 282 |
. . . . . . . . 9
 
 
        |
47 | | leneg 10117 |
. . . . . . . . . . . 12
 
  
    |
48 | 47 | ancoms 455 |
. . . . . . . . . . 11
 
  
    |
49 | 48 | imbi2d 318 |
. . . . . . . . . 10
 
   

 
      |
50 | 49 | ralbidva 2824 |
. . . . . . . . 9
  
 
    
     |
51 | 46, 50 | syl5bbr 263 |
. . . . . . . 8
  
             |
52 | 51 | rexbiia 2888 |
. . . . . . 7
  
        
    |
53 | 36, 52 | bitr4i 256 |
. . . . . 6
  
   
        |
54 | 30, 53 | syl6bb 265 |
. . . . 5

  
         |
55 | 13, 54 | anbi12d 717 |
. . . 4

  

     
         |
56 | | ssrab2 3514 |
. . . . 5
    |
57 | | sup3 10566 |
. . . . 5
              
            
    |
58 | 56, 57 | mp3an1 1351 |
. . . 4
           
            
    |
59 | 55, 58 | syl6bi 232 |
. . 3

  


            
     |
60 | 15 | imbi1d 319 |
. . . . . . . . 9

 
        |
61 | | impexp 448 |
. . . . . . . . 9
   
 

    |
62 | 60, 61 | syl6bb 265 |
. . . . . . . 8

 
        |
63 | 62 | albidv 1767 |
. . . . . . 7

   

         |
64 | | df-ral 2742 |
. . . . . . 7
 
      |
65 | | breq1 4405 |
. . . . . . . . . . 11
  
    |
66 | 65 | notbid 296 |
. . . . . . . . . 10
  
    |
67 | 23, 66 | imbi12d 322 |
. . . . . . . . 9
      
     |
68 | 21, 22, 67 | ralxfr 4618 |
. . . . . . . 8
 

 
      |
69 | | df-ral 2742 |
. . . . . . . 8
 

   

    |
70 | 68, 69 | bitr3i 255 |
. . . . . . 7
 
       
    |
71 | 63, 64, 70 | 3bitr4g 292 |
. . . . . 6

 
  
     |
72 | | breq2 4406 |
. . . . . . . . 9
  
    |
73 | | breq2 4406 |
. . . . . . . . . 10
  
    |
74 | 73 | rexbidv 2901 |
. . . . . . . . 9
   

    |
75 | 72, 74 | imbi12d 322 |
. . . . . . . 8
     
  
     |
76 | 21, 22, 75 | ralxfr 4618 |
. . . . . . 7
 

 
  

    |
77 | | ssel 3426 |
. . . . . . . . . . . . 13

    |
78 | 77 | adantrd 470 |
. . . . . . . . . . . 12

       |
79 | 78 | pm4.71rd 641 |
. . . . . . . . . . 11

   
        |
80 | 79 | exbidv 1768 |
. . . . . . . . . 10

     
   
      |
81 | | df-rex 2743 |
. . . . . . . . . 10
  
  
    |
82 | | renegcl 9937 |
. . . . . . . . . . . 12
    |
83 | | infm3lem 10567 |
. . . . . . . . . . . 12
     |
84 | | eleq1 2517 |
. . . . . . . . . . . . 13
  
    |
85 | | breq1 4405 |
. . . . . . . . . . . . 13
  

     |
86 | 84, 85 | anbi12d 717 |
. . . . . . . . . . . 12
   
   
      |
87 | 82, 83, 86 | rexxfr 4620 |
. . . . . . . . . . 11
    
  
     |
88 | | df-rex 2743 |
. . . . . . . . . . 11
    
   
     |
89 | 87, 88 | bitr3i 255 |
. . . . . . . . . 10
                |
90 | 80, 81, 89 | 3bitr4g 292 |
. . . . . . . . 9

  
  
      |
91 | 90 | imbi2d 318 |
. . . . . . . 8

     
    
       |
92 | 91 | ralbidv 2827 |
. . . . . . 7

 

 
 
  
  
       |
93 | 76, 92 | syl5bb 261 |
. . . . . 6

 

 
  
  
       |
94 | 71, 93 | anbi12d 717 |
. . . . 5

  
 
      
  

 
          |
95 | 94 | rexbidv 2901 |
. . . 4

   
 
   
     
  
  
        |
96 | | breq2 4406 |
. . . . . . . . . 10
   
     |
97 | 96 | notbid 296 |
. . . . . . . . 9
    
    |
98 | 97 | imbi2d 318 |
. . . . . . . 8
        
      |
99 | 98 | ralbidv 2827 |
. . . . . . 7
   
             |
100 | | breq1 4405 |
. . . . . . . . 9
  

     |
101 | 100 | imbi1d 319 |
. . . . . . . 8
           
     
       |
102 | 101 | ralbidv 2827 |
. . . . . . 7
   

       
      
       |
103 | 99, 102 | anbi12d 717 |
. . . . . 6
      
  

 
      
 
    
      
        |
104 | 31, 32, 103 | rexxfr 4620 |
. . . . 5
   
   
  
  
            
      
       |
105 | 39 | imbi1i 327 |
. . . . . . . . . . 11
     
   
   |
106 | | impexp 448 |
. . . . . . . . . . 11
   



 
    |
107 | 105, 106 | bitri 253 |
. . . . . . . . . 10
     

 
    |
108 | 107 | albii 1691 |
. . . . . . . . 9
      
     
    |
109 | | df-ral 2742 |
. . . . . . . . 9
 
            |
110 | | df-ral 2742 |
. . . . . . . . 9
 
 
   
 
    |
111 | 108, 109,
110 | 3bitr4ri 282 |
. . . . . . . 8
 
 
 
     |
112 | | ltneg 10114 |
. . . . . . . . . . 11
 
       |
113 | 112 | notbid 296 |
. . . . . . . . . 10
 
 
     |
114 | 113 | imbi2d 318 |
. . . . . . . . 9
 
   

 
      |
115 | 114 | ralbidva 2824 |
. . . . . . . 8
  
            |
116 | 111, 115 | syl5bbr 263 |
. . . . . . 7
  
            |
117 | | ltneg 10114 |
. . . . . . . . . 10
 
       |
118 | 117 | ancoms 455 |
. . . . . . . . 9
 
       |
119 | | negeq 9867 |
. . . . . . . . . . . . 13
     |
120 | 119 | eleq1d 2513 |
. . . . . . . . . . . 12
  
    |
121 | 120 | rexrab 3202 |
. . . . . . . . . . 11
        
   |
122 | | ltneg 10114 |
. . . . . . . . . . . . 13
 
       |
123 | 122 | anbi2d 710 |
. . . . . . . . . . . 12
 
   

 
      |
124 | 123 | rexbidva 2898 |
. . . . . . . . . . 11
  
 
 
        |
125 | 121, 124 | syl5bb 261 |
. . . . . . . . . 10
  
             |
126 | 125 | adantl 468 |
. . . . . . . . 9
 
                |
127 | 118, 126 | imbi12d 322 |
. . . . . . . 8
 
  
           
       |
128 | 127 | ralbidva 2824 |
. . . . . . 7
  
     
               |
129 | 116, 128 | anbi12d 717 |
. . . . . 6
             
     
                  |
130 | 129 | rexbiia 2888 |
. . . . 5
   
    
      
    
                 |
131 | 104, 130 | bitr4i 256 |
. . . 4
   
   
  
  
          
 
         |
132 | 95, 131 | syl6bb 265 |
. . 3

   
 
   
    
 
          |
133 | 59, 132 | sylibrd 238 |
. 2

  


  
 

     |
134 | 133 | 3impib 1206 |
1
 
  
  
 

    |