Step | Hyp | Ref
| Expression |
1 | | poimirlem2.3 |
. . . . 5
               |
2 | | f1of 5828 |
. . . . 5
            
              |
3 | 1, 2 | syl 17 |
. . . 4
               |
4 | | poimir.0 |
. . . . . . . . 9
   |
5 | 4 | nncnd 10647 |
. . . . . . . 8
   |
6 | | npcan1 10065 |
. . . . . . . 8
       |
7 | 5, 6 | syl 17 |
. . . . . . 7
       |
8 | 4 | nnzd 11062 |
. . . . . . . 8
   |
9 | | peano2zm 11004 |
. . . . . . . 8
 
   |
10 | | uzid 11197 |
. . . . . . . 8
   
    
    |
11 | | peano2uz 11235 |
. . . . . . . 8
      
 
 
          |
12 | 8, 9, 10, 11 | 4syl 19 |
. . . . . . 7
        
    |
13 | 7, 12 | eqeltrrd 2550 |
. . . . . 6
    
    |
14 | | fzss2 11864 |
. . . . . 6
    
 
            |
15 | 13, 14 | syl 17 |
. . . . 5
    
 
      |
16 | | poimirlem1.4 |
. . . . 5
         |
17 | 15, 16 | sseldd 3419 |
. . . 4
       |
18 | 3, 17 | ffvelrnd 6038 |
. . 3
           |
19 | | fzp1elp1 11875 |
. . . . . 6
       
           |
20 | 16, 19 | syl 17 |
. . . . 5
             |
21 | 7 | oveq2d 6324 |
. . . . 5
               |
22 | 20, 21 | eleqtrd 2551 |
. . . 4
         |
23 | 3, 22 | ffvelrnd 6038 |
. . 3
    
        |
24 | | imassrn 5185 |
. . . . . . . . . 10
      
    |
25 | | frn 5747 |
. . . . . . . . . . 11
            
      |
26 | 1, 2, 25 | 3syl 18 |
. . . . . . . . . 10
       |
27 | 24, 26 | syl5ss 3429 |
. . . . . . . . 9
                 |
28 | 27 | sselda 3418 |
. . . . . . . 8
 
          
      |
29 | | poimirlem2.2 |
. . . . . . . . . . 11
           |
30 | 29 | ffvelrnda 6037 |
. . . . . . . . . 10
 
           |
31 | 30 | zred 11063 |
. . . . . . . . 9
 
           |
32 | 31 | ltp1d 10559 |
. . . . . . . . 9
 
                 |
33 | 31, 32 | ltned 9788 |
. . . . . . . 8
 
                 |
34 | 28, 33 | syldan 478 |
. . . . . . 7
 
          
            |
35 | | poimirlem2.1 |
. . . . . . . . . . 11
                 ![]_ ]_](_urbrack.gif) 
                                 |
36 | | breq1 4398 |
. . . . . . . . . . . . . . 15
   
     |
37 | | id 22 |
. . . . . . . . . . . . . . 15
       |
38 | 36, 37 | ifbieq1d 3895 |
. . . . . . . . . . . . . 14
                       |
39 | | elfzelz 11826 |
. . . . . . . . . . . . . . . . . 18
         |
40 | 16, 39 | syl 17 |
. . . . . . . . . . . . . . . . 17
   |
41 | 40 | zred 11063 |
. . . . . . . . . . . . . . . 16
   |
42 | 41 | ltm1d 10561 |
. . . . . . . . . . . . . . 15
     |
43 | 42 | iftrued 3880 |
. . . . . . . . . . . . . 14
                |
44 | 38, 43 | sylan9eqr 2527 |
. . . . . . . . . . . . 13
 

             |
45 | 44 | csbeq1d 3356 |
. . . . . . . . . . . 12
 

           ![]_ ]_](_urbrack.gif) 
                                  ![]_ ]_](_urbrack.gif)                                  |
46 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
     |
47 | | elfzm1b 11898 |
. . . . . . . . . . . . . . . 16
  
      
               |
48 | 40, 46, 47 | syl2anc 673 |
. . . . . . . . . . . . . . 15
                     |
49 | 16, 48 | mpbid 215 |
. . . . . . . . . . . . . 14
             |
50 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . 19
          
    |
51 | 50 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . . 18
                       |
52 | 51 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . 17
                               |
53 | 52 | adantl 473 |
. . . . . . . . . . . . . . . 16
 

                              |
54 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . 20
           |
55 | 40 | zcnd 11064 |
. . . . . . . . . . . . . . . . . . . . 21
   |
56 | | npcan1 10065 |
. . . . . . . . . . . . . . . . . . . . 21
       |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
       |
58 | 54, 57 | sylan9eqr 2527 |
. . . . . . . . . . . . . . . . . . 19
 

      |
59 | 58 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
 

              |
60 | 59 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . 17
 

                      |
61 | 60 | xpeq1d 4862 |
. . . . . . . . . . . . . . . 16
 

                              |
62 | 53, 61 | uneq12d 3580 |
. . . . . . . . . . . . . . 15
 

                                                            |
63 | 62 | oveq2d 6324 |
. . . . . . . . . . . . . 14
 

                                           
                      |
64 | 49, 63 | csbied 3376 |
. . . . . . . . . . . . 13
     ![]_ ]_](_urbrack.gif)                                                                 |
65 | 64 | adantr 472 |
. . . . . . . . . . . 12
 

   
  ![]_ ]_](_urbrack.gif)                                          
                      |
66 | 45, 65 | eqtrd 2505 |
. . . . . . . . . . 11
 

           ![]_ ]_](_urbrack.gif) 
                                                               |
67 | 46 | zcnd 11064 |
. . . . . . . . . . . . . . 15
     |
68 | | npcan1 10065 |
. . . . . . . . . . . . . . 15
             |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
           |
70 | | peano2zm 11004 |
. . . . . . . . . . . . . . 15
         |
71 | | uzid 11197 |
. . . . . . . . . . . . . . 15
                   |
72 | | peano2uz 11235 |
. . . . . . . . . . . . . . 15
            
          
     |
73 | 46, 70, 71, 72 | 4syl 19 |
. . . . . . . . . . . . . 14
                 |
74 | 69, 73 | eqeltrrd 2550 |
. . . . . . . . . . . . 13
             |
75 | | fzss2 11864 |
. . . . . . . . . . . . 13
          
           
    |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
        
        |
77 | 76, 49 | sseldd 3419 |
. . . . . . . . . . 11
           |
78 | | ovex 6336 |
. . . . . . . . . . . 12
          
                     |
79 | 78 | a1i 11 |
. . . . . . . . . . 11
                                  |
80 | 35, 66, 77, 79 | fvmptd 5969 |
. . . . . . . . . 10
    
            
                      |
81 | 80 | fveq1d 5881 |
. . . . . . . . 9
     
                                          |
82 | 81 | adantr 472 |
. . . . . . . 8
 
          
            
                                  |
83 | | ffn 5739 |
. . . . . . . . . . . 12
               |
84 | 29, 83 | syl 17 |
. . . . . . . . . . 11
       |
85 | 84 | adantr 472 |
. . . . . . . . . 10
 
          
      |
86 | | 1ex 9656 |
. . . . . . . . . . . . . . 15
 |
87 | | fnconstg 5784 |
. . . . . . . . . . . . . . 15
                           |
88 | 86, 87 | ax-mp 5 |
. . . . . . . . . . . . . 14
                         |
89 | | c0ex 9655 |
. . . . . . . . . . . . . . 15
 |
90 | | fnconstg 5784 |
. . . . . . . . . . . . . . 15
                       |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . 14
                     |
92 | 88, 91 | pm3.2i 462 |
. . . . . . . . . . . . 13
                                               |
93 | | dff1o3 5834 |
. . . . . . . . . . . . . . . 16
                              |
94 | 93 | simprbi 471 |
. . . . . . . . . . . . . . 15
            
   |
95 | | imain 5669 |
. . . . . . . . . . . . . . 15
 
                       
              |
96 | 1, 94, 95 | 3syl 18 |
. . . . . . . . . . . . . 14
        
                              |
97 | | fzdisj 11852 |
. . . . . . . . . . . . . . . . 17
       
         |
98 | 42, 97 | syl 17 |
. . . . . . . . . . . . . . . 16
               |
99 | 98 | imaeq2d 5174 |
. . . . . . . . . . . . . . 15
        
              |
100 | | ima0 5189 |
. . . . . . . . . . . . . . 15
     |
101 | 99, 100 | syl6eq 2521 |
. . . . . . . . . . . . . 14
        
          |
102 | 96, 101 | eqtr3d 2507 |
. . . . . . . . . . . . 13
        
              |
103 | | fnun 5692 |
. . . . . . . . . . . . 13
                       
                                                                                               |
104 | 92, 102, 103 | sylancr 676 |
. . . . . . . . . . . 12
                                                   |
105 | | elfzuz 11822 |
. . . . . . . . . . . . . . . . . . . 20
             |
106 | 16, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
       |
107 | 57, 106 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . 18
           |
108 | | peano2zm 11004 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
109 | | uzid 11197 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    
    |
110 | | peano2uz 11235 |
. . . . . . . . . . . . . . . . . . . . . 22
      
 
 
          |
111 | 40, 108, 109, 110 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . 21
        
    |
112 | 57, 111 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . . . . 20
    
    |
113 | | peano2uz 11235 |
. . . . . . . . . . . . . . . . . . . 20
    
 
          |
114 | | uzss 11203 |
. . . . . . . . . . . . . . . . . . . 20
      
 
   
          |
115 | 112, 113,
114 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
          
    |
116 | | elfzuz3 11823 |
. . . . . . . . . . . . . . . . . . . . 21
       
       |
117 | | eluzp1p1 11208 |
. . . . . . . . . . . . . . . . . . . . 21
      
 
          |
118 | 16, 116, 117 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
        
    |
119 | 7, 118 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . . . 19
    
    |
120 | 115, 119 | sseldd 3419 |
. . . . . . . . . . . . . . . . . 18
    
    |
121 | | fzsplit2 11850 |
. . . . . . . . . . . . . . . . . 18
                
                      |
122 | 107, 120,
121 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
                       |
123 | 57 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
               |
124 | 123 | uneq2d 3579 |
. . . . . . . . . . . . . . . . 17
                               |
125 | 122, 124 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
                   |
126 | 125 | imaeq2d 5174 |
. . . . . . . . . . . . . . 15
                           |
127 | | imaundi 5254 |
. . . . . . . . . . . . . . 15
                       
             |
128 | 126, 127 | syl6eq 2521 |
. . . . . . . . . . . . . 14
                               |
129 | | f1ofo 5835 |
. . . . . . . . . . . . . . 15
            
              |
130 | | foima 5811 |
. . . . . . . . . . . . . . 15
                           |
131 | 1, 129, 130 | 3syl 18 |
. . . . . . . . . . . . . 14
               |
132 | 128, 131 | eqtr3d 2507 |
. . . . . . . . . . . . 13
        
                  |
133 | 132 | fneq2d 5677 |
. . . . . . . . . . . 12
                                                 
                                   |
134 | 104, 133 | mpbid 215 |
. . . . . . . . . . 11
                                   |
135 | 134 | adantr 472 |
. . . . . . . . . 10
 
          
                                  |
136 | | ovex 6336 |
. . . . . . . . . . 11
     |
137 | 136 | a1i 11 |
. . . . . . . . . 10
 
          
      |
138 | | inidm 3632 |
. . . . . . . . . 10
               |
139 | | eqidd 2472 |
. . . . . . . . . 10
                             |
140 | 102 | adantr 472 |
. . . . . . . . . . . . 13
 
          
                      |
141 | | fzss2 11864 |
. . . . . . . . . . . . . . 15
    
 
            |
142 | | imass2 5210 |
. . . . . . . . . . . . . . 15
                 
             |
143 | 119, 141,
142 | 3syl 18 |
. . . . . . . . . . . . . 14
                     |
144 | 143 | sselda 3418 |
. . . . . . . . . . . . 13
 
          
          |
145 | | fvun2 5952 |
. . . . . . . . . . . . . 14
         
                                            
           
                                                            |
146 | 88, 91, 145 | mp3an12 1380 |
. . . . . . . . . . . . 13
         
           
        
         
                                        |
147 | 140, 144,
146 | syl2anc 673 |
. . . . . . . . . . . 12
 
          
         
                                        |
148 | 89 | fvconst2 6136 |
. . . . . . . . . . . . 13
                           |
149 | 144, 148 | syl 17 |
. . . . . . . . . . . 12
 
          
                  |
150 | 147, 149 | eqtrd 2505 |
. . . . . . . . . . 11
 
          
         
                        |
151 | 150 | adantr 472 |
. . . . . . . . . 10
                                                     |
152 | 85, 135, 137, 137, 138, 139, 151 | ofval 6559 |
. . . . . . . . 9
                                                              |
153 | 28, 152 | mpdan 681 |
. . . . . . . 8
 
          
           
                               |
154 | 30 | zcnd 11064 |
. . . . . . . . . 10
 
           |
155 | 154 | addid1d 9851 |
. . . . . . . . 9
 
                 |
156 | 28, 155 | syldan 478 |
. . . . . . . 8
 
          
            |
157 | 82, 153, 156 | 3eqtrd 2509 |
. . . . . . 7
 
          
                |
158 | | breq1 4398 |
. . . . . . . . . . . . . . 15
 
   |
159 | | oveq1 6315 |
. . . . . . . . . . . . . . 15
       |
160 | 158, 159 | ifbieq2d 3897 |
. . . . . . . . . . . . . 14
                 |
161 | 41 | ltnrd 9786 |
. . . . . . . . . . . . . . 15
   |
162 | 161 | iffalsed 3883 |
. . . . . . . . . . . . . 14
            |
163 | 160, 162 | sylan9eqr 2527 |
. . . . . . . . . . . . 13
 
            |
164 | 163 | csbeq1d 3356 |
. . . . . . . . . . . 12
 
          ![]_ ]_](_urbrack.gif) 
                                  ![]_ ]_](_urbrack.gif)                                  |
165 | | ovex 6336 |
. . . . . . . . . . . . 13
   |
166 | | oveq2 6316 |
. . . . . . . . . . . . . . . . 17
          
    |
167 | 166 | imaeq2d 5174 |
. . . . . . . . . . . . . . . 16
                       |
168 | 167 | xpeq1d 4862 |
. . . . . . . . . . . . . . 15
                               |
169 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
           |
170 | 169 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                   |
171 | 170 | imaeq2d 5174 |
. . . . . . . . . . . . . . . 16
                           |
172 | 171 | xpeq1d 4862 |
. . . . . . . . . . . . . . 15
                                   |
173 | 168, 172 | uneq12d 3580 |
. . . . . . . . . . . . . 14
                                                                 |
174 | 173 | oveq2d 6324 |
. . . . . . . . . . . . 13
                                            
                          |
175 | 165, 174 | csbie 3375 |
. . . . . . . . . . . 12
 
  ![]_ ]_](_urbrack.gif)                                          
                         |
176 | 164, 175 | syl6eq 2521 |
. . . . . . . . . . 11
 
          ![]_ ]_](_urbrack.gif) 
                                                                   |
177 | | 1eluzge0 11226 |
. . . . . . . . . . . . 13
     |
178 | | fzss1 11863 |
. . . . . . . . . . . . 13
    
         
    |
179 | 177, 178 | ax-mp 5 |
. . . . . . . . . . . 12
         
   |
180 | 179, 16 | sseldi 3416 |
. . . . . . . . . . 11
         |
181 | | ovex 6336 |
. . . . . . . . . . . 12
          
                         |
182 | 181 | a1i 11 |
. . . . . . . . . . 11
                                      |
183 | 35, 176, 180, 182 | fvmptd 5969 |
. . . . . . . . . 10
               
                          |
184 | 183 | fveq1d 5881 |
. . . . . . . . 9
                                                  |
185 | 184 | adantr 472 |
. . . . . . . 8
 
          
                                                 |
186 | | fnconstg 5784 |
. . . . . . . . . . . . . . 15
                           |
187 | 86, 186 | ax-mp 5 |
. . . . . . . . . . . . . 14
                         |
188 | | fnconstg 5784 |
. . . . . . . . . . . . . . 15
                               |
189 | 89, 188 | ax-mp 5 |
. . . . . . . . . . . . . 14
                             |
190 | 187, 189 | pm3.2i 462 |
. . . . . . . . . . . . 13
                                                       |
191 | | imain 5669 |
. . . . . . . . . . . . . . . 16
 
                           
                  |
192 | 1, 94, 191 | 3syl 18 |
. . . . . . . . . . . . . . 15
        
                                      |
193 | | peano2re 9824 |
. . . . . . . . . . . . . . . . . . 19
 
   |
194 | 41, 193 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     |
195 | 194 | ltp1d 10559 |
. . . . . . . . . . . . . . . . 17
         |
196 | | fzdisj 11852 |
. . . . . . . . . . . . . . . . 17
           
             |
197 | 195, 196 | syl 17 |
. . . . . . . . . . . . . . . 16
                   |
198 | 197 | imaeq2d 5174 |
. . . . . . . . . . . . . . 15
        
                  |
199 | 192, 198 | eqtr3d 2507 |
. . . . . . . . . . . . . 14
        
                      |
200 | 199, 100 | syl6eq 2521 |
. . . . . . . . . . . . 13
        
                  |
201 | | fnun 5692 |
. . . . . . . . . . . . 13
                       
                                                                                                                   |
202 | 190, 200,
201 | sylancr 676 |
. . . . . . . . . . . 12
                                                           |
203 | | fzsplit 11851 |
. . . . . . . . . . . . . . . . 17
                             |
204 | 22, 203 | syl 17 |
. . . . . . . . . . . . . . . 16
                       |
205 | 204 | imaeq2d 5174 |
. . . . . . . . . . . . . . 15
                               |
206 | | imaundi 5254 |
. . . . . . . . . . . . . . 15
                           
                 |
207 | 205, 206 | syl6eq 2521 |
. . . . . . . . . . . . . 14
                                   |
208 | 207, 131 | eqtr3d 2507 |
. . . . . . . . . . . . 13
        
                      |
209 | 208 | fneq2d 5677 |
. . . . . . . . . . . 12
                                                         
                                       |
210 | 202, 209 | mpbid 215 |
. . . . . . . . . . 11
                                       |
211 | 210 | adantr 472 |
. . . . . . . . . 10
 
          
                                      |
212 | 200 | adantr 472 |
. . . . . . . . . . . . 13
 
          
                          |
213 | | fzss1 11863 |
. . . . . . . . . . . . . . 15
    
              |
214 | | imass2 5210 |
. . . . . . . . . . . . . . 15
                   
               |
215 | 106, 213,
214 | 3syl 18 |
. . . . . . . . . . . . . 14
                 
     |
216 | 215 | sselda 3418 |
. . . . . . . . . . . . 13
 
          
            |
217 | | fvun1 5951 |
. . . . . . . . . . . . . 14
         
                                                    
               
                                                                    |
218 | 187, 189,
217 | mp3an12 1380 |
. . . . . . . . . . . . 13
         
               
          
         
                                              |
219 | 212, 216,
218 | syl2anc 673 |
. . . . . . . . . . . 12
 
          
         
                                              |
220 | 86 | fvconst2 6136 |
. . . . . . . . . . . . 13
       
           
           |
221 | 216, 220 | syl 17 |
. . . . . . . . . . . 12
 
          
                    |
222 | 219, 221 | eqtrd 2505 |
. . . . . . . . . . 11
 
          
         
                            |
223 | 222 | adantr 472 |
. . . . . . . . . 10
                                                         |
224 | 85, 211, 137, 137, 138, 139, 223 | ofval 6559 |
. . . . . . . . 9
                                                                  |
225 | 28, 224 | mpdan 681 |
. . . . . . . 8
 
          
           
                                   |
226 | 185, 225 | eqtrd 2505 |
. . . . . . 7
 
          
                |
227 | 34, 157, 226 | 3netr4d 2720 |
. . . . . 6
 
          
                    |
228 | 227 | ralrimiva 2809 |
. . . . 5
                 
               |
229 | | fzpr 11877 |
. . . . . . . . 9
              |
230 | 16, 39, 229 | 3syl 18 |
. . . . . . . 8
    
         |
231 | 230 | imaeq2d 5174 |
. . . . . . 7
                      |
232 | | f1ofn 5829 |
. . . . . . . . 9
            
      |
233 | 1, 232 | syl 17 |
. . . . . . . 8
       |
234 | | fnimapr 5944 |
. . . . . . . 8
     
    
                        
     |
235 | 233, 17, 22, 234 | syl3anc 1292 |
. . . . . . 7
     
             
     |
236 | 231, 235 | eqtrd 2505 |
. . . . . 6
                    
     |
237 | 236 | raleqdv 2979 |
. . . . 5
                  
            
                                   |
238 | 228, 237 | mpbid 215 |
. . . 4
                   
               |
239 | | fvex 5889 |
. . . . 5
     |
240 | | fvex 5889 |
. . . . 5
       |
241 | | fveq2 5879 |
. . . . . 6
         
                     |
242 | | fveq2 5879 |
. . . . . 6
                           |
243 | 241, 242 | neeq12d 2704 |
. . . . 5
          
            
                             |
244 | | fveq2 5879 |
. . . . . 6
    
      
                       |
245 | | fveq2 5879 |
. . . . . 6
    
                          |
246 | 244, 245 | neeq12d 2704 |
. . . . 5
    
       
            
            
                    |
247 | 239, 240,
243, 246 | ralpr 4016 |
. . . 4
 
         
       
            
     
                                 
                    |
248 | 238, 247 | sylib 201 |
. . 3
                                
                     
      |
249 | 41 | ltp1d 10559 |
. . . . 5
     |
250 | 41, 249 | ltned 9788 |
. . . 4
     |
251 | | f1of1 5827 |
. . . . . . 7
            
              |
252 | 1, 251 | syl 17 |
. . . . . 6
               |
253 | | f1veqaeq 6179 |
. . . . . 6
                  
                        |
254 | 252, 17, 22, 253 | syl12anc 1290 |
. . . . 5
                 |
255 | 254 | necon3d 2664 |
. . . 4
  
              |
256 | 250, 255 | mpd 15 |
. . 3
             |
257 | 243 | anbi1d 719 |
. . . . 5
                             
                                             
                 |
258 | | neeq1 2705 |
. . . . 5
     
       |
259 | 257, 258 | anbi12d 725 |
. . . 4
                         
                   
      
                         
                      |
260 | | fveq2 5879 |
. . . . . . 7
    
      
                       |
261 | | fveq2 5879 |
. . . . . . 7
    
                          |
262 | 260, 261 | neeq12d 2704 |
. . . . . 6
    
       
            
            
                    |
263 | 262 | anbi2d 718 |
. . . . 5
    
                                  
                                             
                     
       |
264 | | neeq2 2706 |
. . . . 5
    
      
             |
265 | 263, 264 | anbi12d 725 |
. . . 4
    
                              
                       
      
                         
                     
                  |
266 | 259, 265 | rspc2ev 3149 |
. . 3
                                                    
                     
                                  
                 
                 |
267 | 18, 23, 248, 256, 266 | syl112anc 1296 |
. 2
                                
                      |
268 | | dfrex2 2837 |
. . 3
                                     
              
                 
                 
                 |
269 | | fveq2 5879 |
. . . . . 6
     
                 |
270 | | fveq2 5879 |
. . . . . 6
                   |
271 | 269, 270 | neeq12d 2704 |
. . . . 5
      
            
                     |
272 | 271 | rmo4 3219 |
. . . 4
           
            
                  
                 
             
   |
273 | | dfral2 2835 |
. . . . . 6
 
                             
              
           
                 
                 |
274 | | df-ne 2643 |
. . . . . . . . 9

  |
275 | 274 | anbi2i 708 |
. . . . . . . 8
                         
                     
                 
             
   |
276 | | annim 432 |
. . . . . . . 8
                         
              
                        
                 |
277 | 275, 276 | bitri 257 |
. . . . . . 7
                         
              
      
                 
                 |
278 | 277 | rexbii 2881 |
. . . . . 6
                               
                          
                 
             
   |
279 | 273, 278 | xchbinxr 318 |
. . . . 5
 
                             
              
            
                 
                 |
280 | 279 | ralbii 2823 |
. . . 4
 
     
                             
                                
                 
                 |
281 | 272, 280 | bitri 257 |
. . 3
           
            
                 
                 
                 |
282 | 268, 281 | xchbinxr 318 |
. 2
                                     
              
                          |
283 | 267, 282 | sylib 201 |
1
                           |