Step | Hyp | Ref
| Expression |
1 | | poimirlem2.3 |
. . . . 5
               |
2 | | f1of 5812 |
. . . . 5
            
              |
3 | 1, 2 | syl 17 |
. . . 4
               |
4 | | poimir.0 |
. . . . . . . . 9
   |
5 | 4 | nncnd 10622 |
. . . . . . . 8
   |
6 | | npcan1 10041 |
. . . . . . . 8
       |
7 | 5, 6 | syl 17 |
. . . . . . 7
       |
8 | 4 | nnzd 11036 |
. . . . . . . 8
   |
9 | | peano2zm 10977 |
. . . . . . . 8
 
   |
10 | | uzid 11170 |
. . . . . . . 8
   
    
    |
11 | | peano2uz 11209 |
. . . . . . . 8
      
 
 
          |
12 | 8, 9, 10, 11 | 4syl 19 |
. . . . . . 7
        
    |
13 | 7, 12 | eqeltrrd 2529 |
. . . . . 6
    
    |
14 | | fzss2 11835 |
. . . . . 6
    
 
            |
15 | 13, 14 | syl 17 |
. . . . 5
    
 
      |
16 | | poimirlem1.4 |
. . . . 5
         |
17 | 15, 16 | sseldd 3432 |
. . . 4
       |
18 | 3, 17 | ffvelrnd 6021 |
. . 3
           |
19 | | fzp1elp1 11846 |
. . . . . 6
       
           |
20 | 16, 19 | syl 17 |
. . . . 5
             |
21 | 7 | oveq2d 6304 |
. . . . 5
               |
22 | 20, 21 | eleqtrd 2530 |
. . . 4
         |
23 | 3, 22 | ffvelrnd 6021 |
. . 3
    
        |
24 | | imassrn 5178 |
. . . . . . . . . 10
      
    |
25 | | frn 5733 |
. . . . . . . . . . 11
            
      |
26 | 1, 2, 25 | 3syl 18 |
. . . . . . . . . 10
       |
27 | 24, 26 | syl5ss 3442 |
. . . . . . . . 9
                 |
28 | 27 | sselda 3431 |
. . . . . . . 8
 
          
      |
29 | | poimirlem2.2 |
. . . . . . . . . . 11
           |
30 | 29 | ffvelrnda 6020 |
. . . . . . . . . 10
 
           |
31 | 30 | zred 11037 |
. . . . . . . . 9
 
           |
32 | 31 | ltp1d 10534 |
. . . . . . . . 9
 
                 |
33 | 31, 32 | ltned 9768 |
. . . . . . . 8
 
                 |
34 | 28, 33 | syldan 473 |
. . . . . . 7
 
          
            |
35 | | poimirlem2.1 |
. . . . . . . . . . 11
                 ![]_ ]_](_urbrack.gif) 
                                 |
36 | | breq1 4404 |
. . . . . . . . . . . . . . 15
   
     |
37 | | id 22 |
. . . . . . . . . . . . . . 15
       |
38 | 36, 37 | ifbieq1d 3903 |
. . . . . . . . . . . . . 14
                       |
39 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . 18
         |
40 | 16, 39 | syl 17 |
. . . . . . . . . . . . . . . . 17
   |
41 | 40 | zred 11037 |
. . . . . . . . . . . . . . . 16
   |
42 | 41 | ltm1d 10536 |
. . . . . . . . . . . . . . 15
     |
43 | 42 | iftrued 3888 |
. . . . . . . . . . . . . 14
                |
44 | 38, 43 | sylan9eqr 2506 |
. . . . . . . . . . . . 13
 

             |
45 | 44 | csbeq1d 3369 |
. . . . . . . . . . . 12
 

           ![]_ ]_](_urbrack.gif) 
                                  ![]_ ]_](_urbrack.gif)                                  |
46 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
     |
47 | | elfzm1b 11869 |
. . . . . . . . . . . . . . . 16
  
      
               |
48 | 40, 46, 47 | syl2anc 666 |
. . . . . . . . . . . . . . 15
                     |
49 | 16, 48 | mpbid 214 |
. . . . . . . . . . . . . 14
             |
50 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . 19
          
    |
51 | 50 | imaeq2d 5167 |
. . . . . . . . . . . . . . . . . 18
                       |
52 | 51 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . 17
                               |
53 | 52 | adantl 468 |
. . . . . . . . . . . . . . . 16
 

                              |
54 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . 20
           |
55 | 40 | zcnd 11038 |
. . . . . . . . . . . . . . . . . . . . 21
   |
56 | | npcan1 10041 |
. . . . . . . . . . . . . . . . . . . . 21
       |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
       |
58 | 54, 57 | sylan9eqr 2506 |
. . . . . . . . . . . . . . . . . . 19
 

      |
59 | 58 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . 18
 

              |
60 | 59 | imaeq2d 5167 |
. . . . . . . . . . . . . . . . 17
 

                      |
61 | 60 | xpeq1d 4856 |
. . . . . . . . . . . . . . . 16
 

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

                                                            |
63 | 62 | oveq2d 6304 |
. . . . . . . . . . . . . 14
 

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

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

           ![]_ ]_](_urbrack.gif) 
                                                               |
67 | 46 | zcnd 11038 |
. . . . . . . . . . . . . . 15
     |
68 | | npcan1 10041 |
. . . . . . . . . . . . . . 15
             |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
           |
70 | | peano2zm 10977 |
. . . . . . . . . . . . . . 15
         |
71 | | uzid 11170 |
. . . . . . . . . . . . . . 15
                   |
72 | | peano2uz 11209 |
. . . . . . . . . . . . . . 15
            
          
     |
73 | 46, 70, 71, 72 | 4syl 19 |
. . . . . . . . . . . . . 14
                 |
74 | 69, 73 | eqeltrrd 2529 |
. . . . . . . . . . . . 13
             |
75 | | fzss2 11835 |
. . . . . . . . . . . . 13
          
           
    |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
        
        |
77 | 76, 49 | sseldd 3432 |
. . . . . . . . . . 11
           |
78 | | ovex 6316 |
. . . . . . . . . . . 12
          
                     |
79 | 78 | a1i 11 |
. . . . . . . . . . 11
                                  |
80 | 35, 66, 77, 79 | fvmptd 5952 |
. . . . . . . . . 10
    
            
                      |
81 | 80 | fveq1d 5865 |
. . . . . . . . 9
     
                                          |
82 | 81 | adantr 467 |
. . . . . . . 8
 
          
            
                                  |
83 | | ffn 5726 |
. . . . . . . . . . . 12
               |
84 | 29, 83 | syl 17 |
. . . . . . . . . . 11
       |
85 | 84 | adantr 467 |
. . . . . . . . . 10
 
          
      |
86 | | 1ex 9635 |
. . . . . . . . . . . . . . 15
 |
87 | | fnconstg 5769 |
. . . . . . . . . . . . . . 15
                           |
88 | 86, 87 | ax-mp 5 |
. . . . . . . . . . . . . 14
                         |
89 | | c0ex 9634 |
. . . . . . . . . . . . . . 15
 |
90 | | fnconstg 5769 |
. . . . . . . . . . . . . . 15
                       |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . 14
                     |
92 | 88, 91 | pm3.2i 457 |
. . . . . . . . . . . . 13
                                               |
93 | | dff1o3 5818 |
. . . . . . . . . . . . . . . 16
                              |
94 | 93 | simprbi 466 |
. . . . . . . . . . . . . . 15
            
   |
95 | | imain 5657 |
. . . . . . . . . . . . . . 15
 
                       
              |
96 | 1, 94, 95 | 3syl 18 |
. . . . . . . . . . . . . 14
        
                              |
97 | | fzdisj 11823 |
. . . . . . . . . . . . . . . . 17
       
         |
98 | 42, 97 | syl 17 |
. . . . . . . . . . . . . . . 16
               |
99 | 98 | imaeq2d 5167 |
. . . . . . . . . . . . . . 15
        
              |
100 | | ima0 5182 |
. . . . . . . . . . . . . . 15
     |
101 | 99, 100 | syl6eq 2500 |
. . . . . . . . . . . . . 14
        
          |
102 | 96, 101 | eqtr3d 2486 |
. . . . . . . . . . . . 13
        
              |
103 | | fnun 5680 |
. . . . . . . . . . . . 13
                       
                                                                                               |
104 | 92, 102, 103 | sylancr 668 |
. . . . . . . . . . . 12
                                                   |
105 | | elfzuz 11793 |
. . . . . . . . . . . . . . . . . . . 20
             |
106 | 16, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
       |
107 | 57, 106 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . 18
           |
108 | | peano2zm 10977 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
109 | | uzid 11170 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    
    |
110 | | peano2uz 11209 |
. . . . . . . . . . . . . . . . . . . . . 22
      
 
 
          |
111 | 40, 108, 109, 110 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . 21
        
    |
112 | 57, 111 | eqeltrrd 2529 |
. . . . . . . . . . . . . . . . . . . 20
    
    |
113 | | peano2uz 11209 |
. . . . . . . . . . . . . . . . . . . 20
    
 
          |
114 | | uzss 11176 |
. . . . . . . . . . . . . . . . . . . 20
      
 
   
          |
115 | 112, 113,
114 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
          
    |
116 | | elfzuz3 11794 |
. . . . . . . . . . . . . . . . . . . . 21
       
       |
117 | | eluzp1p1 11181 |
. . . . . . . . . . . . . . . . . . . . 21
      
 
          |
118 | 16, 116, 117 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
        
    |
119 | 7, 118 | eqeltrrd 2529 |
. . . . . . . . . . . . . . . . . . 19
    
    |
120 | 115, 119 | sseldd 3432 |
. . . . . . . . . . . . . . . . . 18
    
    |
121 | | fzsplit2 11821 |
. . . . . . . . . . . . . . . . . 18
                
                      |
122 | 107, 120,
121 | syl2anc 666 |
. . . . . . . . . . . . . . . . 17
                       |
123 | 57 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . 18
               |
124 | 123 | uneq2d 3587 |
. . . . . . . . . . . . . . . . 17
                               |
125 | 122, 124 | eqtrd 2484 |
. . . . . . . . . . . . . . . 16
                   |
126 | 125 | imaeq2d 5167 |
. . . . . . . . . . . . . . 15
                           |
127 | | imaundi 5247 |
. . . . . . . . . . . . . . 15
                       
             |
128 | 126, 127 | syl6eq 2500 |
. . . . . . . . . . . . . 14
                               |
129 | | f1ofo 5819 |
. . . . . . . . . . . . . . 15
            
              |
130 | | foima 5796 |
. . . . . . . . . . . . . . 15
                           |
131 | 1, 129, 130 | 3syl 18 |
. . . . . . . . . . . . . 14
               |
132 | 128, 131 | eqtr3d 2486 |
. . . . . . . . . . . . 13
        
                  |
133 | 132 | fneq2d 5665 |
. . . . . . . . . . . 12
                                                 
                                   |
134 | 104, 133 | mpbid 214 |
. . . . . . . . . . 11
                                   |
135 | 134 | adantr 467 |
. . . . . . . . . 10
 
          
                                  |
136 | | ovex 6316 |
. . . . . . . . . . 11
     |
137 | 136 | a1i 11 |
. . . . . . . . . 10
 
          
      |
138 | | inidm 3640 |
. . . . . . . . . 10
               |
139 | | eqidd 2451 |
. . . . . . . . . 10
                             |
140 | 102 | adantr 467 |
. . . . . . . . . . . . 13
 
          
                      |
141 | | fzss2 11835 |
. . . . . . . . . . . . . . 15
    
 
            |
142 | | imass2 5203 |
. . . . . . . . . . . . . . 15
                 
             |
143 | 119, 141,
142 | 3syl 18 |
. . . . . . . . . . . . . 14
                     |
144 | 143 | sselda 3431 |
. . . . . . . . . . . . 13
 
          
          |
145 | | fvun2 5935 |
. . . . . . . . . . . . . 14
         
                                            
           
                                                            |
146 | 88, 91, 145 | mp3an12 1353 |
. . . . . . . . . . . . 13
         
           
        
         
                                        |
147 | 140, 144,
146 | syl2anc 666 |
. . . . . . . . . . . 12
 
          
         
                                        |
148 | 89 | fvconst2 6118 |
. . . . . . . . . . . . 13
                           |
149 | 144, 148 | syl 17 |
. . . . . . . . . . . 12
 
          
                  |
150 | 147, 149 | eqtrd 2484 |
. . . . . . . . . . 11
 
          
         
                        |
151 | 150 | adantr 467 |
. . . . . . . . . 10
                                                     |
152 | 85, 135, 137, 137, 138, 139, 151 | ofval 6537 |
. . . . . . . . 9
                                                              |
153 | 28, 152 | mpdan 673 |
. . . . . . . 8
 
          
           
                               |
154 | 30 | zcnd 11038 |
. . . . . . . . . 10
 
           |
155 | 154 | addid1d 9830 |
. . . . . . . . 9
 
                 |
156 | 28, 155 | syldan 473 |
. . . . . . . 8
 
          
            |
157 | 82, 153, 156 | 3eqtrd 2488 |
. . . . . . 7
 
          
                |
158 | | breq1 4404 |
. . . . . . . . . . . . . . 15
 
   |
159 | | oveq1 6295 |
. . . . . . . . . . . . . . 15
       |
160 | 158, 159 | ifbieq2d 3905 |
. . . . . . . . . . . . . 14
                 |
161 | 41 | ltnrd 9766 |
. . . . . . . . . . . . . . 15
   |
162 | 161 | iffalsed 3891 |
. . . . . . . . . . . . . 14
            |
163 | 160, 162 | sylan9eqr 2506 |
. . . . . . . . . . . . 13
 
            |
164 | 163 | csbeq1d 3369 |
. . . . . . . . . . . 12
 
          ![]_ ]_](_urbrack.gif) 
                                  ![]_ ]_](_urbrack.gif)                                  |
165 | | ovex 6316 |
. . . . . . . . . . . . 13
   |
166 | | oveq2 6296 |
. . . . . . . . . . . . . . . . 17
          
    |
167 | 166 | imaeq2d 5167 |
. . . . . . . . . . . . . . . 16
                       |
168 | 167 | xpeq1d 4856 |
. . . . . . . . . . . . . . 15
                               |
169 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . 18
           |
170 | 169 | oveq1d 6303 |
. . . . . . . . . . . . . . . . 17
                   |
171 | 170 | imaeq2d 5167 |
. . . . . . . . . . . . . . . 16
                           |
172 | 171 | xpeq1d 4856 |
. . . . . . . . . . . . . . 15
                                   |
173 | 168, 172 | uneq12d 3588 |
. . . . . . . . . . . . . 14
                                                                 |
174 | 173 | oveq2d 6304 |
. . . . . . . . . . . . 13
                                            
                          |
175 | 165, 174 | csbie 3388 |
. . . . . . . . . . . 12
 
  ![]_ ]_](_urbrack.gif)                                          
                         |
176 | 164, 175 | syl6eq 2500 |
. . . . . . . . . . 11
 
          ![]_ ]_](_urbrack.gif) 
                                                                   |
177 | | 1eluzge0 11199 |
. . . . . . . . . . . . 13
     |
178 | | fzss1 11834 |
. . . . . . . . . . . . 13
    
         
    |
179 | 177, 178 | ax-mp 5 |
. . . . . . . . . . . 12
         
   |
180 | 179, 16 | sseldi 3429 |
. . . . . . . . . . 11
         |
181 | | ovex 6316 |
. . . . . . . . . . . 12
          
                         |
182 | 181 | a1i 11 |
. . . . . . . . . . 11
                                      |
183 | 35, 176, 180, 182 | fvmptd 5952 |
. . . . . . . . . 10
               
                          |
184 | 183 | fveq1d 5865 |
. . . . . . . . 9
                                                  |
185 | 184 | adantr 467 |
. . . . . . . 8
 
          
                                                 |
186 | | fnconstg 5769 |
. . . . . . . . . . . . . . 15
                           |
187 | 86, 186 | ax-mp 5 |
. . . . . . . . . . . . . 14
                         |
188 | | fnconstg 5769 |
. . . . . . . . . . . . . . 15
                               |
189 | 89, 188 | ax-mp 5 |
. . . . . . . . . . . . . 14
                             |
190 | 187, 189 | pm3.2i 457 |
. . . . . . . . . . . . 13
                                                       |
191 | | imain 5657 |
. . . . . . . . . . . . . . . 16
 
                           
                  |
192 | 1, 94, 191 | 3syl 18 |
. . . . . . . . . . . . . . 15
        
                                      |
193 | | peano2re 9803 |
. . . . . . . . . . . . . . . . . . 19
 
   |
194 | 41, 193 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     |
195 | 194 | ltp1d 10534 |
. . . . . . . . . . . . . . . . 17
         |
196 | | fzdisj 11823 |
. . . . . . . . . . . . . . . . 17
           
             |
197 | 195, 196 | syl 17 |
. . . . . . . . . . . . . . . 16
                   |
198 | 197 | imaeq2d 5167 |
. . . . . . . . . . . . . . 15
        
                  |
199 | 192, 198 | eqtr3d 2486 |
. . . . . . . . . . . . . 14
        
                      |
200 | 199, 100 | syl6eq 2500 |
. . . . . . . . . . . . 13
        
                  |
201 | | fnun 5680 |
. . . . . . . . . . . . 13
                       
                                                                                                                   |
202 | 190, 200,
201 | sylancr 668 |
. . . . . . . . . . . 12
                                                           |
203 | | fzsplit 11822 |
. . . . . . . . . . . . . . . . 17
                             |
204 | 22, 203 | syl 17 |
. . . . . . . . . . . . . . . 16
                       |
205 | 204 | imaeq2d 5167 |
. . . . . . . . . . . . . . 15
                               |
206 | | imaundi 5247 |
. . . . . . . . . . . . . . 15
                           
                 |
207 | 205, 206 | syl6eq 2500 |
. . . . . . . . . . . . . 14
                                   |
208 | 207, 131 | eqtr3d 2486 |
. . . . . . . . . . . . 13
        
                      |
209 | 208 | fneq2d 5665 |
. . . . . . . . . . . 12
                                                         
                                       |
210 | 202, 209 | mpbid 214 |
. . . . . . . . . . 11
                                       |
211 | 210 | adantr 467 |
. . . . . . . . . 10
 
          
                                      |
212 | 200 | adantr 467 |
. . . . . . . . . . . . 13
 
          
                          |
213 | | fzss1 11834 |
. . . . . . . . . . . . . . 15
    
              |
214 | | imass2 5203 |
. . . . . . . . . . . . . . 15
                   
               |
215 | 106, 213,
214 | 3syl 18 |
. . . . . . . . . . . . . 14
                 
     |
216 | 215 | sselda 3431 |
. . . . . . . . . . . . 13
 
          
            |
217 | | fvun1 5934 |
. . . . . . . . . . . . . 14
         
                                                    
               
                                                                    |
218 | 187, 189,
217 | mp3an12 1353 |
. . . . . . . . . . . . 13
         
               
          
         
                                              |
219 | 212, 216,
218 | syl2anc 666 |
. . . . . . . . . . . 12
 
          
         
                                              |
220 | 86 | fvconst2 6118 |
. . . . . . . . . . . . 13
       
           
           |
221 | 216, 220 | syl 17 |
. . . . . . . . . . . 12
 
          
                    |
222 | 219, 221 | eqtrd 2484 |
. . . . . . . . . . 11
 
          
         
                            |
223 | 222 | adantr 467 |
. . . . . . . . . 10
                                                         |
224 | 85, 211, 137, 137, 138, 139, 223 | ofval 6537 |
. . . . . . . . 9
                                                                  |
225 | 28, 224 | mpdan 673 |
. . . . . . . 8
 
          
           
                                   |
226 | 185, 225 | eqtrd 2484 |
. . . . . . 7
 
          
                |
227 | 34, 157, 226 | 3netr4d 2700 |
. . . . . 6
 
          
                    |
228 | 227 | ralrimiva 2801 |
. . . . 5
                 
               |
229 | | fzpr 11848 |
. . . . . . . . 9
              |
230 | 16, 39, 229 | 3syl 18 |
. . . . . . . 8
    
         |
231 | 230 | imaeq2d 5167 |
. . . . . . 7
                      |
232 | | f1ofn 5813 |
. . . . . . . . 9
            
      |
233 | 1, 232 | syl 17 |
. . . . . . . 8
       |
234 | | fnimapr 5927 |
. . . . . . . 8
     
    
                        
     |
235 | 233, 17, 22, 234 | syl3anc 1267 |
. . . . . . 7
     
             
     |
236 | 231, 235 | eqtrd 2484 |
. . . . . 6
                    
     |
237 | 236 | raleqdv 2992 |
. . . . 5
                  
            
                                   |
238 | 228, 237 | mpbid 214 |
. . . 4
                   
               |
239 | | fvex 5873 |
. . . . 5
     |
240 | | fvex 5873 |
. . . . 5
       |
241 | | fveq2 5863 |
. . . . . 6
         
                     |
242 | | fveq2 5863 |
. . . . . 6
                           |
243 | 241, 242 | neeq12d 2684 |
. . . . 5
          
            
                             |
244 | | fveq2 5863 |
. . . . . 6
    
      
                       |
245 | | fveq2 5863 |
. . . . . 6
    
                          |
246 | 244, 245 | neeq12d 2684 |
. . . . 5
    
       
            
            
                    |
247 | 239, 240,
243, 246 | ralpr 4024 |
. . . 4
 
         
       
            
     
                                 
                    |
248 | 238, 247 | sylib 200 |
. . 3
                                
                     
      |
249 | 41 | ltp1d 10534 |
. . . . 5
     |
250 | 41, 249 | ltned 9768 |
. . . 4
     |
251 | | f1of1 5811 |
. . . . . . 7
            
              |
252 | 1, 251 | syl 17 |
. . . . . 6
               |
253 | | f1veqaeq 6159 |
. . . . . 6
                  
                        |
254 | 252, 17, 22, 253 | syl12anc 1265 |
. . . . 5
                 |
255 | 254 | necon3d 2644 |
. . . 4
  
              |
256 | 250, 255 | mpd 15 |
. . 3
             |
257 | 243 | anbi1d 710 |
. . . . 5
                             
                                             
                 |
258 | | neeq1 2685 |
. . . . 5
     
       |
259 | 257, 258 | anbi12d 716 |
. . . 4
                         
                   
      
                         
                      |
260 | | fveq2 5863 |
. . . . . . 7
    
      
                       |
261 | | fveq2 5863 |
. . . . . . 7
    
                          |
262 | 260, 261 | neeq12d 2684 |
. . . . . 6
    
       
            
            
                    |
263 | 262 | anbi2d 709 |
. . . . 5
    
                                  
                                             
                     
       |
264 | | neeq2 2686 |
. . . . 5
    
      
             |
265 | 263, 264 | anbi12d 716 |
. . . 4
    
                              
                       
      
                         
                     
                  |
266 | 259, 265 | rspc2ev 3160 |
. . 3
                                                    
                     
                                  
                 
                 |
267 | 18, 23, 248, 256, 266 | syl112anc 1271 |
. 2
                                
                      |
268 | | dfrex2 2837 |
. . 3
                                     
              
                 
                 
                 |
269 | | fveq2 5863 |
. . . . . 6
     
                 |
270 | | fveq2 5863 |
. . . . . 6
                   |
271 | 269, 270 | neeq12d 2684 |
. . . . 5
      
            
                     |
272 | 271 | rmo4 3230 |
. . . 4
           
            
                  
                 
             
   |
273 | | dfral2 2834 |
. . . . . 6
 
                             
              
           
                 
                 |
274 | | df-ne 2623 |
. . . . . . . . 9

  |
275 | 274 | anbi2i 699 |
. . . . . . . 8
                         
                     
                 
             
   |
276 | | annim 427 |
. . . . . . . 8
                         
              
                        
                 |
277 | 275, 276 | bitri 253 |
. . . . . . 7
                         
              
      
                 
                 |
278 | 277 | rexbii 2888 |
. . . . . 6
                               
                          
                 
             
   |
279 | 273, 278 | xchbinxr 313 |
. . . . 5
 
                             
              
            
                 
                 |
280 | 279 | ralbii 2818 |
. . . 4
 
     
                             
                                
                 
                 |
281 | 272, 280 | bitri 253 |
. . 3
           
            
                 
                 
                 |
282 | 268, 281 | xchbinxr 313 |
. 2
                                     
              
                          |
283 | 267, 282 | sylib 200 |
1
                           |