Step | Hyp | Ref
| Expression |
1 | | elequ1 1904 |
. . . . . . . . . . . . . . . 16
 
   |
2 | | elequ2 1911 |
. . . . . . . . . . . . . . . 16
 
   |
3 | 1, 2 | bitrd 261 |
. . . . . . . . . . . . . . 15
 
   |
4 | 3 | notbid 300 |
. . . . . . . . . . . . . 14
 
   |
5 | 4 | cbvralv 3030 |
. . . . . . . . . . . . 13
 

  |
6 | 5 | biimpi 199 |
. . . . . . . . . . . 12
 

  |
7 | 6 | ralimi 2792 |
. . . . . . . . . . 11
 
            
             
  |
8 | | untuni 30384 |
. . . . . . . . . . 11
 
            
            
  |
9 | 7, 8 | sylibr 217 |
. . . . . . . . . 10
 
            
  


       
  |
10 | | vex 3059 |
. . . . . . . . . . . 12
 |
11 | | sseq1 3464 |
. . . . . . . . . . . . 13
 
   |
12 | | treq 4516 |
. . . . . . . . . . . . 13
 
   |
13 | | raleq 2998 |
. . . . . . . . . . . . 13
  
     

         |
14 | 11, 12, 13 | 3anbi123d 1348 |
. . . . . . . . . . . 12
   
      
            |
15 | 10, 14 | elab 3196 |
. . . . . . . . . . 11
   
         
         |
16 | | vex 3059 |
. . . . . . . . . . . . . . . 16
 |
17 | | dfon2lem3 30479 |
. . . . . . . . . . . . . . . 16
        

    |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . . 15
       

   |
19 | 18 | simprd 469 |
. . . . . . . . . . . . . 14
       
  |
20 | | untelirr 30383 |
. . . . . . . . . . . . . 14
 
  |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
      
  |
22 | 21 | ralimi 2792 |
. . . . . . . . . . . 12
 
      
  |
23 | 22 | 3ad2ant3 1037 |
. . . . . . . . . . 11
 

       
  |
24 | 15, 23 | sylbi 200 |
. . . . . . . . . 10
   
        
  |
25 | 9, 24 | mprg 2762 |
. . . . . . . . 9
    
         |
26 | | untelirr 30383 |
. . . . . . . . . 10
 
           
                          |
27 | | psseq2 3532 |
. . . . . . . . . . . . . . . . . 18
 
   |
28 | 27 | anbi1d 716 |
. . . . . . . . . . . . . . . . 17
   
     |
29 | | elequ2 1911 |
. . . . . . . . . . . . . . . . 17
 
   |
30 | 28, 29 | imbi12d 326 |
. . . . . . . . . . . . . . . 16
             |
31 | 30 | albidv 1777 |
. . . . . . . . . . . . . . 15
       
         |
32 | 31 | cbvralv 3030 |
. . . . . . . . . . . . . 14
 
     

        |
33 | 32 | 3anbi3i 1207 |
. . . . . . . . . . . . 13
 

      
           |
34 | 33 | abbii 2577 |
. . . . . . . . . . . 12
             
         |
35 | 34 | unieqi 4220 |
. . . . . . . . . . 11
             


         |
36 | 35 | eleq2i 2531 |
. . . . . . . . . 10
  


          

       
                          |
37 | 26, 36 | sylnib 310 |
. . . . . . . . 9
 
           
                          |
38 | 25, 37 | ax-mp 5 |
. . . . . . . 8
 


          

         |
39 | | dfon2lem7.1 |
. . . . . . . . . 10
 |
40 | | dfon2lem2 30478 |
. . . . . . . . . 10
             |
41 | 39, 40 | ssexi 4561 |
. . . . . . . . 9
             |
42 | 41 | snss 4108 |
. . . . . . . 8
  


          

       
                

          |
43 | 38, 42 | mtbi 304 |
. . . . . . 7
   

            
         |
44 | 43 | intnan 930 |
. . . . . 6
   

          

            
        
              |
45 | | df-suc 5447 |
. . . . . . . 8
 


            
                        |
46 | 45 | sseq1i 3467 |
. . . . . . 7
   

          

       
  


            
                        |
47 | | unss 3619 |
. . . . . . 7
     
           
                        

                                        
          |
48 | 46, 47 | bitr4i 260 |
. . . . . 6
   

          

       
  


          

            
        
               |
49 | 44, 48 | mtbir 305 |
. . . . 5
  

          

         |
50 | 41 | snss 4108 |
. . . . . 6
  


                     
  |
51 | 45 | sseq1i 3467 |
. . . . . . . . 9
   

                                      |
52 | | unss 3619 |
. . . . . . . . 9
     
           

         
  


            
            |
53 | 51, 52 | bitr4i 260 |
. . . . . . . 8
   

                        

            |
54 | | dfon2lem1 30477 |
. . . . . . . . . . . 12
 


         |
55 | | suctr 5524 |
. . . . . . . . . . . 12
    
       
              |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . 11
  

         |
57 | | vex 3059 |
. . . . . . . . . . . . . 14
 |
58 | 57 | elsuc 5510 |
. . . . . . . . . . . . 13
            
    
         


           |
59 | | eluni2 4215 |
. . . . . . . . . . . . . . 15
             
              |
60 | | nfa1 1989 |
. . . . . . . . . . . . . . . 16
         |
61 | 31 | rspccv 3158 |
. . . . . . . . . . . . . . . . . . 19
 
                |
62 | | psseq1 3531 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
63 | | treq 4516 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
64 | 62, 63 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
65 | | elequ1 1904 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
66 | 64, 65 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . 20
             |
67 | 66 | cbvalv 2126 |
. . . . . . . . . . . . . . . . . . 19
      
        |
68 | 61, 67 | syl6ib 234 |
. . . . . . . . . . . . . . . . . 18
 
                |
69 | 68 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . 17
 

                 |
70 | 15, 69 | sylbi 200 |
. . . . . . . . . . . . . . . 16
   
        
         |
71 | 60, 70 | rexlimi 2880 |
. . . . . . . . . . . . . . 15
                      |
72 | 59, 71 | sylbi 200 |
. . . . . . . . . . . . . 14
                
    |
73 | | psseq1 3531 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
74 | | treq 4516 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
75 | 73, 74 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
     |
76 | | elequ1 1904 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
77 | 75, 76 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
78 | 77 | cbvalv 2126 |
. . . . . . . . . . . . . . . . . . . . . 22
      
        |
79 | 61, 78 | syl6ib 234 |
. . . . . . . . . . . . . . . . . . . . 21
 
                |
80 | 79 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . . . . 20
 

                 |
81 | 15, 80 | sylbi 200 |
. . . . . . . . . . . . . . . . . . 19
   
        
         |
82 | 81 | rexlimiv 2884 |
. . . . . . . . . . . . . . . . . 18
                      |
83 | 59, 82 | sylbi 200 |
. . . . . . . . . . . . . . . . 17
                
    |
84 | 83 | rgen 2758 |
. . . . . . . . . . . . . . . 16
    
            
   |
85 | | dfon2lem6 30482 |
. . . . . . . . . . . . . . . 16
                  
            
          
          


           |
86 | 54, 84, 85 | mp2an 683 |
. . . . . . . . . . . . . . 15
      

            
          |
87 | | psseq2 3532 |
. . . . . . . . . . . . . . . . . 18
             
               |
88 | 87 | anbi1d 716 |
. . . . . . . . . . . . . . . . 17
               
    
            |
89 | | eleq2 2528 |
. . . . . . . . . . . . . . . . 17
             
               |
90 | 88, 89 | imbi12d 326 |
. . . . . . . . . . . . . . . 16
               
 
 
              


            |
91 | 90 | albidv 1777 |
. . . . . . . . . . . . . . 15
                       
              


            |
92 | 86, 91 | mpbiri 241 |
. . . . . . . . . . . . . 14
                
    |
93 | 72, 92 | jaoi 385 |
. . . . . . . . . . . . 13
                 
        
        |
94 | 58, 93 | sylbi 200 |
. . . . . . . . . . . 12
                     |
95 | 94 | rgen 2758 |
. . . . . . . . . . 11
                 
   |
96 | 41 | sucex 6664 |
. . . . . . . . . . . . 13
 


         |
97 | | sseq1 3464 |
. . . . . . . . . . . . . 14
             
               |
98 | | treq 4516 |
. . . . . . . . . . . . . 14
             
               |
99 | | raleq 2998 |
. . . . . . . . . . . . . 14
              
     
                 
     |
100 | 97, 98, 99 | 3anbi123d 1348 |
. . . . . . . . . . . . 13
               
      
   

         


          


                   |
101 | 96, 100 | elab 3196 |
. . . . . . . . . . . 12
   

               
  
   

         


          


                  |
102 | | elssuni 4240 |
. . . . . . . . . . . 12
   

               
     

          

          |
103 | 101, 102 | sylbir 218 |
. . . . . . . . . . 11
                 
            
            
      
           
          |
104 | 56, 95, 103 | mp3an23 1365 |
. . . . . . . . . 10
   

       
               
          |
105 | | sseq1 3464 |
. . . . . . . . . . . . 13
 
   |
106 | | treq 4516 |
. . . . . . . . . . . . 13
 
   |
107 | | raleq 2998 |
. . . . . . . . . . . . . 14
  
     

         |
108 | | psseq1 3531 |
. . . . . . . . . . . . . . . . . 18
 
   |
109 | | treq 4516 |
. . . . . . . . . . . . . . . . . 18
 
   |
110 | 108, 109 | anbi12d 722 |
. . . . . . . . . . . . . . . . 17
   
     |
111 | | elequ1 1904 |
. . . . . . . . . . . . . . . . 17
 
   |
112 | 110, 111 | imbi12d 326 |
. . . . . . . . . . . . . . . 16
             |
113 | 112 | cbvalv 2126 |
. . . . . . . . . . . . . . 15
      
        |
114 | 113 | ralbii 2830 |
. . . . . . . . . . . . . 14
 
     

        |
115 | 107, 114 | syl6bb 269 |
. . . . . . . . . . . . 13
  
     

         |
116 | 105, 106,
115 | 3anbi123d 1348 |
. . . . . . . . . . . 12
   
      
            |
117 | 116 | cbvabv 2585 |
. . . . . . . . . . 11
             
         |
118 | 117 | unieqi 4220 |
. . . . . . . . . 10
        
    


         |
119 | 104, 118 | syl6sseq 3489 |
. . . . . . . . 9
   

       
               
          |
120 | 119 | a1i 11 |
. . . . . . . 8
           
          

          

           |
121 | 53, 120 | syl5bir 226 |
. . . . . . 7
                        

            

          

           |
122 | 40, 121 | mpani 687 |
. . . . . 6
            
        
  

          

           |
123 | 50, 122 | syl5bi 225 |
. . . . 5
          

       
               
           |
124 | 49, 123 | mtoi 183 |
. . . 4
         

          |
125 | | psseq1 3531 |
. . . . . . . 8
                 
           |
126 | | treq 4516 |
. . . . . . . 8
                 
           |
127 | 125, 126 | anbi12d 722 |
. . . . . . 7
               
  


                        |
128 | | eleq1 2527 |
. . . . . . 7
                 
           |
129 | 127, 128 | imbi12d 326 |
. . . . . 6
               
 
    

                       

            |
130 | 41, 129 | spcv 3151 |
. . . . 5
                       

            
           |
131 | 54, 130 | mpan2i 688 |
. . . 4
          

           
           |
132 | 124, 131 | mtod 182 |
. . 3
         

          |
133 | | dfpss2 3529 |
. . . . 5
  


                       

           |
134 | 133 | biimpri 211 |
. . . 4
     
          

                       |
135 | 40, 134 | mpan 681 |
. . 3
    
                      |
136 | 132, 135 | nsyl2 132 |
. 2
                     |
137 | | eluni2 4215 |
. . . . 5
             
              |
138 | | psseq2 3532 |
. . . . . . . . . . . . . 14
 
   |
139 | 138 | anbi1d 716 |
. . . . . . . . . . . . 13
   
     |
140 | | elequ2 1911 |
. . . . . . . . . . . . 13
 
   |
141 | 139, 140 | imbi12d 326 |
. . . . . . . . . . . 12
             |
142 | 141 | albidv 1777 |
. . . . . . . . . . 11
       
         |
143 | 142 | cbvralv 3030 |
. . . . . . . . . 10
 
     

        |
144 | 13, 143 | syl6bb 269 |
. . . . . . . . 9
  
     

         |
145 | 11, 12, 144 | 3anbi123d 1348 |
. . . . . . . 8
   
      
            |
146 | 10, 145 | elab 3196 |
. . . . . . 7
   
         
         |
147 | | rsp 2765 |
. . . . . . . 8
 
                |
148 | 147 | 3ad2ant3 1037 |
. . . . . . 7
 

                 |
149 | 146, 148 | sylbi 200 |
. . . . . 6
   
        
         |
150 | 149 | rexlimiv 2884 |
. . . . 5
                      |
151 | 137, 150 | sylbi 200 |
. . . 4
                
    |
152 | 151 | rgen 2758 |
. . 3
    
            
   |
153 | | raleq 2998 |
. . 3
  


             
            
 

         |
154 | 152, 153 | mpbii 216 |
. 2
  


                 |
155 | | psseq2 3532 |
. . . . . 6
 
   |
156 | 155 | anbi1d 716 |
. . . . 5
   
     |
157 | | eleq2 2528 |
. . . . 5
 
   |
158 | 156, 157 | imbi12d 326 |
. . . 4
             |
159 | 158 | albidv 1777 |
. . 3
       
         |
160 | 159 | rspccv 3158 |
. 2
 
      
         |
161 | 136, 154,
160 | 3syl 18 |
1
       
         |