Proof of Theorem poimirlem11
Step | Hyp | Ref
| Expression |
1 | | eldif 3400 |
. . . . . . 7
                                                   
                   |
2 | | imassrn 5185 |
. . . . . . . . . . . 12
                         |
3 | | poimirlem12.2 |
. . . . . . . . . . . . . . . . . 18
   |
4 | | elrabi 3181 |
. . . . . . . . . . . . . . . . . . 19
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
5 | | poimirlem22.s |
. . . . . . . . . . . . . . . . . . 19
     ..^                                              ![]_ ]_](_urbrack.gif)                                                           |
6 | 4, 5 | eleq2s 2567 |
. . . . . . . . . . . . . . . . . 18
     ..^                            |
7 | 3, 6 | syl 17 |
. . . . . . . . . . . . . . . . 17
     ..^                            |
8 | | xp1st 6842 |
. . . . . . . . . . . . . . . . 17
     ..^                                 ..^                       |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . . . 16
        ..^                       |
10 | | xp2nd 6843 |
. . . . . . . . . . . . . . . 16
        ..^                                             |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . 15
                         |
12 | | fvex 5889 |
. . . . . . . . . . . . . . . 16
         |
13 | | f1oeq1 5818 |
. . . . . . . . . . . . . . . 16
                                             |
14 | 12, 13 | elab 3173 |
. . . . . . . . . . . . . . 15
                      
                      |
15 | 11, 14 | sylib 201 |
. . . . . . . . . . . . . 14
                       |
16 | | f1of 5828 |
. . . . . . . . . . . . . 14
                    
                      |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
                       |
18 | | frn 5747 |
. . . . . . . . . . . . 13
                                   |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . 12
               |
20 | 2, 19 | syl5ss 3429 |
. . . . . . . . . . 11
                       |
21 | | poimirlem11.4 |
. . . . . . . . . . . . . . . . 17
   |
22 | | elrabi 3181 |
. . . . . . . . . . . . . . . . . 18
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
23 | 22, 5 | eleq2s 2567 |
. . . . . . . . . . . . . . . . 17
     ..^                            |
24 | 21, 23 | syl 17 |
. . . . . . . . . . . . . . . 16
     ..^                            |
25 | | xp1st 6842 |
. . . . . . . . . . . . . . . 16
     ..^                                 ..^                       |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . 15
        ..^                       |
27 | | xp2nd 6843 |
. . . . . . . . . . . . . . 15
        ..^                                             |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
                         |
29 | | fvex 5889 |
. . . . . . . . . . . . . . 15
         |
30 | | f1oeq1 5818 |
. . . . . . . . . . . . . . 15
                                             |
31 | 29, 30 | elab 3173 |
. . . . . . . . . . . . . 14
                      
                      |
32 | 28, 31 | sylib 201 |
. . . . . . . . . . . . 13
                       |
33 | | f1ofo 5835 |
. . . . . . . . . . . . 13
                    
                      |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
                       |
35 | | foima 5811 |
. . . . . . . . . . . 12
                                           |
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
                       |
37 | 20, 36 | sseqtr4d 3455 |
. . . . . . . . . 10
                                   |
38 | 37 | ssdifd 3558 |
. . . . . . . . 9
                                  
                                    |
39 | | dff1o3 5834 |
. . . . . . . . . . . . 13
                                         
            |
40 | 39 | simprbi 471 |
. . . . . . . . . . . 12
                    
           |
41 | 32, 40 | syl 17 |
. . . . . . . . . . 11
            |
42 | | imadif 5668 |
. . . . . . . . . . 11
                         
                                          |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
                                                           |
44 | | difun2 3838 |
. . . . . . . . . . . 12
                               |
45 | | poimirlem11.6 |
. . . . . . . . . . . . . . 15
       |
46 | | fzsplit 11851 |
. . . . . . . . . . . . . . 15
                       |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . 14
                   |
48 | | uncom 3569 |
. . . . . . . . . . . . . 14
                         |
49 | 47, 48 | syl6eq 2521 |
. . . . . . . . . . . . 13
                   |
50 | 49 | difeq1d 3539 |
. . . . . . . . . . . 12
                               |
51 | | incom 3616 |
. . . . . . . . . . . . . 14
                         |
52 | | elfznn 11854 |
. . . . . . . . . . . . . . . . . 18
       |
53 | 45, 52 | syl 17 |
. . . . . . . . . . . . . . . . 17
   |
54 | 53 | nnred 10646 |
. . . . . . . . . . . . . . . 16
   |
55 | 54 | ltp1d 10559 |
. . . . . . . . . . . . . . 15
     |
56 | | fzdisj 11852 |
. . . . . . . . . . . . . . 15
       
 
       |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . 14
               |
58 | 51, 57 | syl5eq 2517 |
. . . . . . . . . . . . 13
               |
59 | | disj3 3813 |
. . . . . . . . . . . . 13
       
    
            
       |
60 | 58, 59 | sylib 201 |
. . . . . . . . . . . 12
                     |
61 | 44, 50, 60 | 3eqtr4a 2531 |
. . . . . . . . . . 11
                   |
62 | 61 | imaeq2d 5174 |
. . . . . . . . . 10
                                           |
63 | 43, 62 | eqtr3d 2507 |
. . . . . . . . 9
                                                       |
64 | 38, 63 | sseqtrd 3454 |
. . . . . . . 8
                                  
                    |
65 | 64 | sselda 3418 |
. . . . . . 7
 
                                                       |
66 | 1, 65 | sylan2br 484 |
. . . . . 6
 
                
                 
                    |
67 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
68 | 67 | breq2d 4407 |
. . . . . . . . . . . . . . . . . 18
 
   
       |
69 | 68 | ifbid 3894 |
. . . . . . . . . . . . . . . . 17
                         |
70 | 69 | csbeq1d 3356 |
. . . . . . . . . . . . . . . 16
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
71 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
72 | 71 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
                   |
73 | 71 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
74 | 73 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
75 | 74 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . 19
                                           |
76 | 73 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . 20
                                       |
77 | 76 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . 19
                                               |
78 | 75, 77 | uneq12d 3580 |
. . . . . . . . . . . . . . . . . 18
                                                                                           |
79 | 72, 78 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
                                                                                                                 |
80 | 79 | csbeq2dv 3785 |
. . . . . . . . . . . . . . . 16
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
81 | 70, 80 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
82 | 81 | mpteq2dv 4483 |
. . . . . . . . . . . . . 14
                     ![]_ ]_](_urbrack.gif)                                                                             ![]_ ]_](_urbrack.gif)                                                           |
83 | 82 | eqeq2d 2481 |
. . . . . . . . . . . . 13
 
    
               ![]_ ]_](_urbrack.gif)                                                        
                    ![]_ ]_](_urbrack.gif)                                                            |
84 | 83, 5 | elrab2 3186 |
. . . . . . . . . . . 12

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
85 | 84 | simprbi 471 |
. . . . . . . . . . 11
     
               ![]_ ]_](_urbrack.gif)                                                           |
86 | 21, 85 | syl 17 |
. . . . . . . . . 10
                     ![]_ ]_](_urbrack.gif)                                                           |
87 | | poimirlem11.5 |
. . . . . . . . . . . . . . . 16
       |
88 | | breq12 4400 |
. . . . . . . . . . . . . . . 16
             
     |
89 | 87, 88 | sylan2 482 |
. . . . . . . . . . . . . . 15
    
          |
90 | 89 | ancoms 460 |
. . . . . . . . . . . . . 14
 

  
   
     |
91 | | oveq1 6315 |
. . . . . . . . . . . . . . 15
           |
92 | 53 | nncnd 10647 |
. . . . . . . . . . . . . . . 16
   |
93 | | npcan1 10065 |
. . . . . . . . . . . . . . . 16
       |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . 15
       |
95 | 91, 94 | sylan9eqr 2527 |
. . . . . . . . . . . . . 14
 

      |
96 | 90, 95 | ifbieq2d 3897 |
. . . . . . . . . . . . 13
 

                      |
97 | 53 | nnzd 11062 |
. . . . . . . . . . . . . . . . . . 19
   |
98 | | poimir.0 |
. . . . . . . . . . . . . . . . . . . 20
   |
99 | 98 | nnzd 11062 |
. . . . . . . . . . . . . . . . . . 19
   |
100 | | elfzm1b 11898 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
101 | 97, 99, 100 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
                 |
102 | 45, 101 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
           |
103 | | elfzle1 11828 |
. . . . . . . . . . . . . . . . 17
             |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . 16

    |
105 | | 0red 9662 |
. . . . . . . . . . . . . . . . 17
   |
106 | | nnm1nn0 10935 |
. . . . . . . . . . . . . . . . . . 19
 
   |
107 | 53, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     |
108 | 107 | nn0red 10950 |
. . . . . . . . . . . . . . . . 17
     |
109 | 105, 108 | lenltd 9798 |
. . . . . . . . . . . . . . . 16
  
      |
110 | 104, 109 | mpbid 215 |
. . . . . . . . . . . . . . 15
     |
111 | 110 | iffalsed 3883 |
. . . . . . . . . . . . . 14
          |
112 | 111 | adantr 472 |
. . . . . . . . . . . . 13
 

           |
113 | 96, 112 | eqtrd 2505 |
. . . . . . . . . . . 12
 

               |
114 | 113 | csbeq1d 3356 |
. . . . . . . . . . 11
 

               ![]_ ]_](_urbrack.gif)                                                          ![]_ ]_](_urbrack.gif)                                                          |
115 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . 18
           |
116 | 115 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . 17
                                   |
117 | 116 | xpeq1d 4862 |
. . . . . . . . . . . . . . . 16
                                           |
118 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . 19
       |
119 | 118 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
               |
120 | 119 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . 17
                                       |
121 | 120 | xpeq1d 4862 |
. . . . . . . . . . . . . . . 16
                                               |
122 | 117, 121 | uneq12d 3580 |
. . . . . . . . . . . . . . 15
                                                                                           |
123 | 122 | oveq2d 6324 |
. . . . . . . . . . . . . 14
                                                                                                                 |
124 | 123 | adantl 473 |
. . . . . . . . . . . . 13
 
                                                                                                                 |
125 | 45, 124 | csbied 3376 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)                                                                                                                 |
126 | 125 | adantr 472 |
. . . . . . . . . . 11
 

    ![]_ ]_](_urbrack.gif)                                                                                                                 |
127 | 114, 126 | eqtrd 2505 |
. . . . . . . . . 10
 

               ![]_ ]_](_urbrack.gif)                                                                                                                 |
128 | | ovex 6336 |
. . . . . . . . . . 11
                                                        |
129 | 128 | a1i 11 |
. . . . . . . . . 10
                                                          |
130 | 86, 127, 102, 129 | fvmptd 5969 |
. . . . . . . . 9
    
                                                           |
131 | 130 | fveq1d 5881 |
. . . . . . . 8
     
                                                                  |
132 | 131 | adantr 472 |
. . . . . . 7
 
                                                                                          |
133 | | imassrn 5185 |
. . . . . . . . . 10
                           |
134 | | f1of 5828 |
. . . . . . . . . . . 12
                    
                      |
135 | 32, 134 | syl 17 |
. . . . . . . . . . 11
                       |
136 | | frn 5747 |
. . . . . . . . . . 11
                                   |
137 | 135, 136 | syl 17 |
. . . . . . . . . 10
               |
138 | 133, 137 | syl5ss 3429 |
. . . . . . . . 9
                         |
139 | 138 | sselda 3418 |
. . . . . . . 8
 
                         |
140 | | xp1st 6842 |
. . . . . . . . . . . 12
        ..^                               ..^        |
141 | 26, 140 | syl 17 |
. . . . . . . . . . 11
           ..^        |
142 | | elmapfn 7512 |
. . . . . . . . . . 11
           ..^                    |
143 | 141, 142 | syl 17 |
. . . . . . . . . 10
               |
144 | 143 | adantr 472 |
. . . . . . . . 9
 
                                 |
145 | | 1ex 9656 |
. . . . . . . . . . . . . 14
 |
146 | | fnconstg 5784 |
. . . . . . . . . . . . . 14
                                       |
147 | 145, 146 | ax-mp 5 |
. . . . . . . . . . . . 13
                                     |
148 | | c0ex 9655 |
. . . . . . . . . . . . . 14
 |
149 | | fnconstg 5784 |
. . . . . . . . . . . . . 14
                                           |
150 | 148, 149 | ax-mp 5 |
. . . . . . . . . . . . 13
                                         |
151 | 147, 150 | pm3.2i 462 |
. . . . . . . . . . . 12
                                                                               |
152 | | imain 5669 |
. . . . . . . . . . . . . 14
                         
 
                                            |
153 | 41, 152 | syl 17 |
. . . . . . . . . . . . 13
                                                               |
154 | 57 | imaeq2d 5174 |
. . . . . . . . . . . . . 14
                                       |
155 | | ima0 5189 |
. . . . . . . . . . . . . 14
             |
156 | 154, 155 | syl6eq 2521 |
. . . . . . . . . . . . 13
                           |
157 | 153, 156 | eqtr3d 2507 |
. . . . . . . . . . . 12
                                       |
158 | | fnun 5692 |
. . . . . . . . . . . 12
                                                                                                                                                                                                       |
159 | 151, 157,
158 | sylancr 676 |
. . . . . . . . . . 11
                                                                                   |
160 | | imaundi 5254 |
. . . . . . . . . . . . 13
                                                             |
161 | 47 | imaeq2d 5174 |
. . . . . . . . . . . . . 14
                                           |
162 | 161, 36 | eqtr3d 2507 |
. . . . . . . . . . . . 13
                               |
163 | 160, 162 | syl5eqr 2519 |
. . . . . . . . . . . 12
                                           |
164 | 163 | fneq2d 5677 |
. . . . . . . . . . 11
                                                                                                                                     |
165 | 159, 164 | mpbid 215 |
. . . . . . . . . 10
                                                   |
166 | 165 | adantr 472 |
. . . . . . . . 9
 
                                                                     |
167 | | ovex 6336 |
. . . . . . . . . 10
     |
168 | 167 | a1i 11 |
. . . . . . . . 9
 
                         |
169 | | inidm 3632 |
. . . . . . . . 9
               |
170 | | eqidd 2472 |
. . . . . . . . 9
                          
                          |
171 | | fvun2 5952 |
. . . . . . . . . . . . 13
                                                                                                                  
                   
                                                                            |
172 | 147, 150,
171 | mp3an12 1380 |
. . . . . . . . . . . 12
                                                                                                                                     |
173 | 157, 172 | sylan 479 |
. . . . . . . . . . 11
 
                                                                                               |
174 | 148 | fvconst2 6136 |
. . . . . . . . . . . 12
                  
                            |
175 | 174 | adantl 473 |
. . . . . . . . . . 11
 
                                               |
176 | 173, 175 | eqtrd 2505 |
. . . . . . . . . 10
 
                                                                     |
177 | 176 | adantr 472 |
. . . . . . . . 9
                          
                                                  |
178 | 144, 166,
168, 168, 169, 170, 177 | ofval 6559 |
. . . . . . . 8
                          
                                                                           |
179 | 139, 178 | mpdan 681 |
. . . . . . 7
 
                                                                                              |
180 | | elmapi 7511 |
. . . . . . . . . . . . 13
           ..^                       ..^   |
181 | 141, 180 | syl 17 |
. . . . . . . . . . . 12
                  ..^   |
182 | 181 | ffvelrnda 6037 |
. . . . . . . . . . 11
 
                  ..^   |
183 | | elfzonn0 11988 |
. . . . . . . . . . 11
              ..^               |
184 | 182, 183 | syl 17 |
. . . . . . . . . 10
 
                   |
185 | 184 | nn0cnd 10951 |
. . . . . . . . 9
 
                   |
186 | 139, 185 | syldan 478 |
. . . . . . . 8
 
                                 |
187 | 186 | addid1d 9851 |
. . . . . . 7
 
                                               |
188 | 132, 179,
187 | 3eqtrd 2509 |
. . . . . 6
 
                                           |
189 | 66, 188 | syldan 478 |
. . . . 5
 
                
                 
                        |
190 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
191 | 190 | breq2d 4407 |
. . . . . . . . . . . . . . . . . 18
 
   
       |
192 | 191 | ifbid 3894 |
. . . . . . . . . . . . . . . . 17
                         |
193 | 192 | csbeq1d 3356 |
. . . . . . . . . . . . . . . 16
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
194 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
195 | 194 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
                   |
196 | 194 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
197 | 196 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
198 | 197 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . 19
                                           |
199 | 196 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . 20
                                       |
200 | 199 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . 19
                                               |
201 | 198, 200 | uneq12d 3580 |
. . . . . . . . . . . . . . . . . 18
                                                                                           |
202 | 195, 201 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
                                                                                                                 |
203 | 202 | csbeq2dv 3785 |
. . . . . . . . . . . . . . . 16
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
204 | 193, 203 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
205 | 204 | mpteq2dv 4483 |
. . . . . . . . . . . . . 14
                     ![]_ ]_](_urbrack.gif)                                                                             ![]_ ]_](_urbrack.gif)                                                           |
206 | 205 | eqeq2d 2481 |
. . . . . . . . . . . . 13
 
    
               ![]_ ]_](_urbrack.gif)                                                        
                    ![]_ ]_](_urbrack.gif)                                                            |
207 | 206, 5 | elrab2 3186 |
. . . . . . . . . . . 12

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
208 | 207 | simprbi 471 |
. . . . . . . . . . 11
     
               ![]_ ]_](_urbrack.gif)                                                           |
209 | 3, 208 | syl 17 |
. . . . . . . . . 10
                     ![]_ ]_](_urbrack.gif)                                                           |
210 | | poimirlem11.3 |
. . . . . . . . . . . . . . . 16
       |
211 | | breq12 4400 |
. . . . . . . . . . . . . . . 16
             
     |
212 | 210, 211 | sylan2 482 |
. . . . . . . . . . . . . . 15
    
          |
213 | 212 | ancoms 460 |
. . . . . . . . . . . . . 14
 

  
   
     |
214 | 213, 95 | ifbieq2d 3897 |
. . . . . . . . . . . . 13
 

                      |
215 | 214, 112 | eqtrd 2505 |
. . . . . . . . . . . 12
 

               |
216 | 215 | csbeq1d 3356 |
. . . . . . . . . . 11
 

               ![]_ ]_](_urbrack.gif)                                                          ![]_ ]_](_urbrack.gif)                                                          |
217 | 115 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . 17
                                   |
218 | 217 | xpeq1d 4862 |
. . . . . . . . . . . . . . . 16
                                           |
219 | 119 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . 17
                                       |
220 | 219 | xpeq1d 4862 |
. . . . . . . . . . . . . . . 16
                                               |
221 | 218, 220 | uneq12d 3580 |
. . . . . . . . . . . . . . 15
                                                                                           |
222 | 221 | oveq2d 6324 |
. . . . . . . . . . . . . 14
                                                                                                                 |
223 | 222 | adantl 473 |
. . . . . . . . . . . . 13
 
                                                                                                                 |
224 | 45, 223 | csbied 3376 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)                                                                                                                 |
225 | 224 | adantr 472 |
. . . . . . . . . . 11
 

    ![]_ ]_](_urbrack.gif)                                                                                                                 |
226 | 216, 225 | eqtrd 2505 |
. . . . . . . . . 10
 

               ![]_ ]_](_urbrack.gif)                                                                                                                 |
227 | | ovex 6336 |
. . . . . . . . . . 11
                                                        |
228 | 227 | a1i 11 |
. . . . . . . . . 10
                                                          |
229 | 209, 226,
102, 228 | fvmptd 5969 |
. . . . . . . . 9
    
                                                           |
230 | 229 | fveq1d 5881 |
. . . . . . . 8
     
                                                                  |
231 | 230 | adantr 472 |
. . . . . . 7
 
                                                                                        |
232 | 20 | sselda 3418 |
. . . . . . . 8
 
                       |
233 | | xp1st 6842 |
. . . . . . . . . . . 12
        ..^                               ..^        |
234 | 9, 233 | syl 17 |
. . . . . . . . . . 11
           ..^        |
235 | | elmapfn 7512 |
. . . . . . . . . . 11
           ..^                    |
236 | 234, 235 | syl 17 |
. . . . . . . . . 10
               |
237 | 236 | adantr 472 |
. . . . . . . . 9
 
                               |
238 | | fnconstg 5784 |
. . . . . . . . . . . . . 14
                                       |
239 | 145, 238 | ax-mp 5 |
. . . . . . . . . . . . 13
                                     |
240 | | fnconstg 5784 |
. . . . . . . . . . . . . 14
                                           |
241 | 148, 240 | ax-mp 5 |
. . . . . . . . . . . . 13
                                         |
242 | 239, 241 | pm3.2i 462 |
. . . . . . . . . . . 12
                                                                               |
243 | | dff1o3 5834 |
. . . . . . . . . . . . . . . 16
                                         
            |
244 | 243 | simprbi 471 |
. . . . . . . . . . . . . . 15
                    
           |
245 | 15, 244 | syl 17 |
. . . . . . . . . . . . . 14
            |
246 | | imain 5669 |
. . . . . . . . . . . . . 14
                         
 
                                            |
247 | 245, 246 | syl 17 |
. . . . . . . . . . . . 13
                                                               |
248 | 57 | imaeq2d 5174 |
. . . . . . . . . . . . . 14
                                       |
249 | | ima0 5189 |
. . . . . . . . . . . . . 14
             |
250 | 248, 249 | syl6eq 2521 |
. . . . . . . . . . . . 13
                           |
251 | 247, 250 | eqtr3d 2507 |
. . . . . . . . . . . 12
                                       |
252 | | fnun 5692 |
. . . . . . . . . . . 12
                                                                                                                                                                                                       |
253 | 242, 251,
252 | sylancr 676 |
. . . . . . . . . . 11
                                                                                   |
254 | | imaundi 5254 |
. . . . . . . . . . . . 13
                                                             |
255 | 47 | imaeq2d 5174 |
. . . . . . . . . . . . . 14
                    |