Step | Hyp | Ref
| Expression |
1 | | isfi 7593 |
. . . . . . 7

   |
2 | | ensym 7618 |
. . . . . . . . 9
   |
3 | | breq1 4405 |
. . . . . . . . . . . . . . . 16


   |
4 | 3 | anbi2d 710 |
. . . . . . . . . . . . . . 15

  
 
 
     |
5 | 4 | imbi1d 319 |
. . . . . . . . . . . . . 14

      
   
 
     |
6 | 5 | albidv 1767 |
. . . . . . . . . . . . 13

     
   
      
     |
7 | | breq1 4405 |
. . . . . . . . . . . . . . . 16
 
   |
8 | 7 | anbi2d 710 |
. . . . . . . . . . . . . . 15
     
 
     |
9 | 8 | imbi1d 319 |
. . . . . . . . . . . . . 14
        
  
  
    |
10 | 9 | albidv 1767 |
. . . . . . . . . . . . 13
      
   
            |
11 | | breq1 4405 |
. . . . . . . . . . . . . . . 16
     |
12 | 11 | anbi2d 710 |
. . . . . . . . . . . . . . 15
     
 
     |
13 | 12 | imbi1d 319 |
. . . . . . . . . . . . . 14
    
   
  

      |
14 | 13 | albidv 1767 |
. . . . . . . . . . . . 13
         
     

      |
15 | | ensym 7618 |
. . . . . . . . . . . . . . . . . . . 20

  |
16 | | en0 7632 |
. . . . . . . . . . . . . . . . . . . 20

  |
17 | 15, 16 | sylib 200 |
. . . . . . . . . . . . . . . . . . 19

  |
18 | 17 | anim1i 572 |
. . . . . . . . . . . . . . . . . 18
       |
19 | 18 | ancoms 455 |
. . . . . . . . . . . . . . . . 17
  
    |
20 | 19 | adantll 720 |
. . . . . . . . . . . . . . . 16
  
      |
21 | | df-ne 2624 |
. . . . . . . . . . . . . . . . 17

  |
22 | | pm3.24 893 |
. . . . . . . . . . . . . . . . . 18

  |
23 | 22 | pm2.21i 135 |
. . . . . . . . . . . . . . . . 17
 
 
  |
24 | 21, 23 | sylan2b 478 |
. . . . . . . . . . . . . . . 16
      |
25 | 20, 24 | syl 17 |
. . . . . . . . . . . . . . 15
  
     |
26 | 25 | ax-gen 1669 |
. . . . . . . . . . . . . 14
      
   |
27 | 26 | a1i 11 |
. . . . . . . . . . . . 13
 



      
    |
28 | | nfv 1761 |
. . . . . . . . . . . . . . 15
  

   |
29 | | nfa1 1979 |
. . . . . . . . . . . . . . 15
      
     |
30 | | bren 7578 |
. . . . . . . . . . . . . . . . . . 19

       |
31 | | f1of 5814 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
32 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
33 | 32 | sucid 5502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
34 | | ffvelrn 6020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             |
35 | 31, 33, 34 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
36 | | ssel 3426 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
37 | 35, 36 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
38 | 37 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
           |
39 | 38 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
     
    


         |
40 | | df-ne 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
      |
41 | | imassrn 5179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
42 | | dff1o2 5819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    
     |
43 | 42 | simp3bi 1025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    
  |
44 | 41, 43 | syl5sseq 3480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
        
  |
45 | | sstr2 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
       |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         
   |
47 | 46 | anim1d 568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                         |
48 | | f1of1 5813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           |
49 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
50 | | sssucid 5500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 |
51 | | f1imaen2g 7630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
        
 
      |
52 | 50, 32, 51 | mpanr12 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     

      |
53 | 48, 49, 52 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
        
  |
54 | 53 | ensymd 7620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
      |
55 | 47, 54 | jctird 547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                               |
56 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 |
57 | | imaexg 6730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
59 | | sseq1 3453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     
       |
60 | | neeq1 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     
       |
61 | 59, 60 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      

             |
62 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
       |
63 | 61, 62 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         
     
             |
64 | | inteq 4237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             |
65 | 64 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
        |
66 | 63, 65 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
            
                          |
67 | 58, 66 | spcv 3140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
                             |
68 | 55, 67 | sylan9 663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
  
                 |
69 | | ineq1 3627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
             
   |
70 | 69 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                   |
71 | | ineq2 3628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
          
              |
72 | 71 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
            
     
        |
73 | 70, 72 | rspc2v 3159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             

                |
74 | 73 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                               |
75 | 68, 74 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          
  
                                   |
76 | 75 | com4r 89 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 



          
  
                              |
77 | 76 | exp5c 621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 



             


    
    
     
            |
78 | 77 | com14 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              

 



    
    
     
            |
79 | 78 | imp43 600 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
     
    


                            |
80 | 40, 79 | syl5bir 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
     
    


            
     
         |
81 | | inteq 4237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
        |
82 | | int0 4248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  |
83 | 81, 82 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
       |
84 | 83 | ineq1d 3633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
     
             |
85 | | ssv 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
86 | | sseqin2 3651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
            |
87 | 85, 86 | mpbi 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
88 | 84, 87 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
     
           |
89 | 88 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
           
       |
90 | 89 | biimprd 227 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
          
        |
91 | 80, 90 | pm2.61d2 164 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
     
    


                      |
92 | 39, 91 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
       
     
    


                |
93 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
94 | 93 | intunsn 4274 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                         |
95 | | f1ofn 5815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
96 | | fnsnfv 5925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
               |
97 | 95, 33, 96 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
98 | 97 | uneq2d 3588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                               |
99 | | df-suc 5429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
100 | 99 | imaeq2i 5166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
          |
101 | | imaundi 5248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                     |
102 | 100, 101 | eqtr2i 2474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
              
  |
103 | 98, 102 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                       |
104 | | f1ofo 5821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
105 | | foima 5798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
107 | 103, 106 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
108 | 107 | inteqd 4239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                     |
109 | 94, 108 | syl5eqr 2499 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
110 | 109 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     |
111 | 110 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . 22
       
     
    


                   |
112 | 92, 111 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . 21
       
     
    


   
  |
113 | 112 | exp43 617 |
. . . . . . . . . . . . . . . . . . . 20
              

 



      |
114 | 113 | exlimdv 1779 |
. . . . . . . . . . . . . . . . . . 19
  
   
     
     

  
     |
115 | 30, 114 | syl5bi 221 |
. . . . . . . . . . . . . . . . . 18
 
        

 



      |
116 | 115 | imp 431 |
. . . . . . . . . . . . . . . . 17
 
            

  
    |
117 | 116 | adantlr 721 |
. . . . . . . . . . . . . . . 16
  

            

  
    |
118 | 117 | com13 83 |
. . . . . . . . . . . . . . 15
 



     
       
      |
119 | 28, 29, 118 | alrimd 1959 |
. . . . . . . . . . . . . 14
 



     
           
    |
120 | 119 | a1i 11 |
. . . . . . . . . . . . 13
  

          

       
     |
121 | 6, 10, 14, 27, 120 | finds2 6721 |
. . . . . . . . . . . 12
  

      
       |
122 | | sp 1937 |
. . . . . . . . . . . 12
     
         
   |
123 | 121, 122 | syl6 34 |
. . . . . . . . . . 11
  

            |
124 | 123 | exp4a 611 |
. . . . . . . . . 10
  

            |
125 | 124 | com24 90 |
. . . . . . . . 9
 
 
            |
126 | 2, 125 | syl5 33 |
. . . . . . . 8
 
 
            |
127 | 126 | rexlimiv 2873 |
. . . . . . 7
 
 
  

  
    |
128 | 1, 127 | sylbi 199 |
. . . . . 6
  
           |
129 | 128 | com13 83 |
. . . . 5
 



 
       |
130 | 129 | impd 433 |
. . . 4
 



  

     |
131 | 130 | alrimiv 1773 |
. . 3
 



           |
132 | | zfpair2 4640 |
. . . . . 6
    |
133 | | sseq1 3453 |
. . . . . . . . 9
    
      |
134 | | neeq1 2686 |
. . . . . . . . 9
    
      |
135 | 133, 134 | anbi12d 717 |
. . . . . . . 8
     

           |
136 | | eleq1 2517 |
. . . . . . . 8
    
      |
137 | 135, 136 | anbi12d 717 |
. . . . . . 7
       
                 |
138 | | inteq 4237 |
. . . . . . . 8
           |
139 | 138 | eleq1d 2513 |
. . . . . . 7
     
   
   |
140 | 137, 139 | imbi12d 322 |
. . . . . 6
           
                      |
141 | 132, 140 | spcv 3140 |
. . . . 5
     
                         |
142 | | vex 3048 |
. . . . . . 7
 |
143 | | vex 3048 |
. . . . . . 7
 |
144 | 142, 143 | prss 4126 |
. . . . . 6
 
      |
145 | 142 | prnz 4091 |
. . . . . . 7
    |
146 | 145 | biantru 508 |
. . . . . 6
              |
147 | | prfi 7846 |
. . . . . . 7
    |
148 | 147 | biantru 508 |
. . . . . 6
        
               |
149 | 144, 146,
148 | 3bitrri 276 |
. . . . 5
             

   |
150 | 142, 143 | intpr 4268 |
. . . . . 6
       |
151 | 150 | eleq1i 2520 |
. . . . 5
    
    |
152 | 141, 149,
151 | 3imtr3g 273 |
. . . 4
     
     

     |
153 | 152 | ralrimivv 2808 |
. . 3
     
    

    |
154 | 131, 153 | impbii 191 |
. 2
 



    

     |
155 | | ineq1 3627 |
. . . 4
 
     |
156 | 155 | eleq1d 2513 |
. . 3
   
     |
157 | | ineq2 3628 |
. . . 4
 
     |
158 | 157 | eleq1d 2513 |
. . 3
   
     |
159 | 156, 158 | cbvral2v 3027 |
. 2
 



 
    |
160 | | df-3an 987 |
. . . 4
 

 
    |
161 | 160 | imbi1i 327 |
. . 3
  
  
  

     |
162 | 161 | albii 1691 |
. 2
       
           |
163 | 154, 159,
162 | 3bitr4i 281 |
1
 



   
     |