Proof of Theorem poimirlem12
Step | Hyp | Ref
| Expression |
1 | | eldif 3413 |
. . . . . . 7
                                                   
                   |
2 | | imassrn 5178 |
. . . . . . . . . . . 12
                         |
3 | | poimirlem12.2 |
. . . . . . . . . . . . . . . 16
   |
4 | | elrabi 3192 |
. . . . . . . . . . . . . . . . 17
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
5 | | poimirlem22.s |
. . . . . . . . . . . . . . . . 17
     ..^                                              ![]_ ]_](_urbrack.gif)                                                           |
6 | 4, 5 | eleq2s 2546 |
. . . . . . . . . . . . . . . 16
     ..^                            |
7 | | xp1st 6820 |
. . . . . . . . . . . . . . . 16
     ..^                                 ..^                       |
8 | 3, 6, 7 | 3syl 18 |
. . . . . . . . . . . . . . 15
        ..^                       |
9 | | xp2nd 6821 |
. . . . . . . . . . . . . . 15
        ..^                                             |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . 14
                         |
11 | | fvex 5873 |
. . . . . . . . . . . . . . 15
         |
12 | | f1oeq1 5803 |
. . . . . . . . . . . . . . 15
                                             |
13 | 11, 12 | elab 3184 |
. . . . . . . . . . . . . 14
                      
                      |
14 | 10, 13 | sylib 200 |
. . . . . . . . . . . . 13
                       |
15 | | f1of 5812 |
. . . . . . . . . . . . 13
                    
                      |
16 | | frn 5733 |
. . . . . . . . . . . . 13
                                   |
17 | 14, 15, 16 | 3syl 18 |
. . . . . . . . . . . 12
               |
18 | 2, 17 | syl5ss 3442 |
. . . . . . . . . . 11
                       |
19 | | poimirlem12.4 |
. . . . . . . . . . . . . . 15
   |
20 | | elrabi 3192 |
. . . . . . . . . . . . . . . 16
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
21 | 20, 5 | eleq2s 2546 |
. . . . . . . . . . . . . . 15
     ..^                            |
22 | | xp1st 6820 |
. . . . . . . . . . . . . . 15
     ..^                                 ..^                       |
23 | 19, 21, 22 | 3syl 18 |
. . . . . . . . . . . . . 14
        ..^                       |
24 | | xp2nd 6821 |
. . . . . . . . . . . . . 14
        ..^                                             |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
                         |
26 | | fvex 5873 |
. . . . . . . . . . . . . 14
         |
27 | | f1oeq1 5803 |
. . . . . . . . . . . . . 14
                                             |
28 | 26, 27 | elab 3184 |
. . . . . . . . . . . . 13
                      
                      |
29 | 25, 28 | sylib 200 |
. . . . . . . . . . . 12
                       |
30 | | f1ofo 5819 |
. . . . . . . . . . . 12
                    
                      |
31 | | foima 5796 |
. . . . . . . . . . . 12
                                           |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . 11
                       |
33 | 18, 32 | sseqtr4d 3468 |
. . . . . . . . . 10
                                   |
34 | 33 | ssdifd 3568 |
. . . . . . . . 9
                                  
                                    |
35 | | dff1o3 5818 |
. . . . . . . . . . . 12
                                         
            |
36 | 35 | simprbi 466 |
. . . . . . . . . . 11
                    
           |
37 | | imadif 5656 |
. . . . . . . . . . 11
                         
                                          |
38 | 29, 36, 37 | 3syl 18 |
. . . . . . . . . 10
                                                           |
39 | | difun2 3846 |
. . . . . . . . . . . 12
                               |
40 | | poimirlem12.6 |
. . . . . . . . . . . . . . . . 17
         |
41 | | elfznn0 11884 |
. . . . . . . . . . . . . . . . 17
         |
42 | | nn0p1nn 10906 |
. . . . . . . . . . . . . . . . 17

    |
43 | 40, 41, 42 | 3syl 18 |
. . . . . . . . . . . . . . . 16
     |
44 | | nnuz 11191 |
. . . . . . . . . . . . . . . 16
     |
45 | 43, 44 | syl6eleq 2538 |
. . . . . . . . . . . . . . 15
         |
46 | | poimir.0 |
. . . . . . . . . . . . . . . . . 18
   |
47 | 46 | nncnd 10622 |
. . . . . . . . . . . . . . . . 17
   |
48 | | npcan1 10041 |
. . . . . . . . . . . . . . . . 17
       |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
       |
50 | | elfzuz3 11794 |
. . . . . . . . . . . . . . . . 17
       
       |
51 | | peano2uz 11209 |
. . . . . . . . . . . . . . . . 17
      
 
        |
52 | 40, 50, 51 | 3syl 18 |
. . . . . . . . . . . . . . . 16
           |
53 | 49, 52 | eqeltrrd 2529 |
. . . . . . . . . . . . . . 15
       |
54 | | fzsplit2 11821 |
. . . . . . . . . . . . . . 15
            
                  |
55 | 45, 53, 54 | syl2anc 666 |
. . . . . . . . . . . . . 14
                   |
56 | | uncom 3577 |
. . . . . . . . . . . . . 14
                         |
57 | 55, 56 | syl6eq 2500 |
. . . . . . . . . . . . 13
                   |
58 | 57 | difeq1d 3549 |
. . . . . . . . . . . 12
                               |
59 | | incom 3624 |
. . . . . . . . . . . . . 14
                         |
60 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . 17
   |
61 | 60 | nn0red 10923 |
. . . . . . . . . . . . . . . 16
   |
62 | 61 | ltp1d 10534 |
. . . . . . . . . . . . . . 15
     |
63 | | fzdisj 11823 |
. . . . . . . . . . . . . . 15
       
 
       |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . 14
               |
65 | 59, 64 | syl5eq 2496 |
. . . . . . . . . . . . 13
               |
66 | | disj3 3808 |
. . . . . . . . . . . . 13
       
    
            
       |
67 | 65, 66 | sylib 200 |
. . . . . . . . . . . 12
                     |
68 | 39, 58, 67 | 3eqtr4a 2510 |
. . . . . . . . . . 11
                   |
69 | 68 | imaeq2d 5167 |
. . . . . . . . . 10
                                           |
70 | 38, 69 | eqtr3d 2486 |
. . . . . . . . 9
                                                       |
71 | 34, 70 | sseqtrd 3467 |
. . . . . . . 8
                                  
                    |
72 | 71 | sselda 3431 |
. . . . . . 7
 
                                                       |
73 | 1, 72 | sylan2br 479 |
. . . . . 6
 
                
                 
                    |
74 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . 19
           |
75 | 74 | breq2d 4413 |
. . . . . . . . . . . . . . . . . 18
 
   
       |
76 | 75 | ifbid 3902 |
. . . . . . . . . . . . . . . . 17
                         |
77 | 76 | csbeq1d 3369 |
. . . . . . . . . . . . . . . 16
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
78 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . 19
           |
79 | 78 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . 18
                   |
80 | 78 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
81 | 80 | imaeq1d 5166 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
82 | 81 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . 19
                                           |
83 | 80 | imaeq1d 5166 |
. . . . . . . . . . . . . . . . . . . 20
                                       |
84 | 83 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . 19
                                               |
85 | 82, 84 | uneq12d 3588 |
. . . . . . . . . . . . . . . . . 18
                                                                                           |
86 | 79, 85 | oveq12d 6306 |
. . . . . . . . . . . . . . . . 17
                                                                                                                 |
87 | 86 | csbeq2dv 3780 |
. . . . . . . . . . . . . . . 16
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
88 | 77, 87 | eqtrd 2484 |
. . . . . . . . . . . . . . 15
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
89 | 88 | mpteq2dv 4489 |
. . . . . . . . . . . . . 14
                     ![]_ ]_](_urbrack.gif)                                                                             ![]_ ]_](_urbrack.gif)                                                           |
90 | 89 | eqeq2d 2460 |
. . . . . . . . . . . . 13
 
    
               ![]_ ]_](_urbrack.gif)                                                        
                    ![]_ ]_](_urbrack.gif)                                                            |
91 | 90, 5 | elrab2 3197 |
. . . . . . . . . . . 12

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
92 | 91 | simprbi 466 |
. . . . . . . . . . 11
     
               ![]_ ]_](_urbrack.gif)                                                           |
93 | 19, 92 | syl 17 |
. . . . . . . . . 10
                     ![]_ ]_](_urbrack.gif)                                                           |
94 | | breq1 4404 |
. . . . . . . . . . . . . 14
 
   
       |
95 | | id 22 |
. . . . . . . . . . . . . 14
   |
96 | 94, 95 | ifbieq1d 3903 |
. . . . . . . . . . . . 13
                         |
97 | 46 | nnred 10621 |
. . . . . . . . . . . . . . . . 17
   |
98 | | peano2rem 9938 |
. . . . . . . . . . . . . . . . 17
 
   |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . . 16
     |
100 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . 17
           |
101 | 40, 100 | syl 17 |
. . . . . . . . . . . . . . . 16

    |
102 | 97 | ltm1d 10536 |
. . . . . . . . . . . . . . . 16
     |
103 | 61, 99, 97, 101, 102 | lelttrd 9790 |
. . . . . . . . . . . . . . 15
   |
104 | | poimirlem12.5 |
. . . . . . . . . . . . . . 15
       |
105 | 103, 104 | breqtrrd 4428 |
. . . . . . . . . . . . . 14
       |
106 | 105 | iftrued 3888 |
. . . . . . . . . . . . 13
              |
107 | 96, 106 | sylan9eqr 2506 |
. . . . . . . . . . . 12
 
              |
108 | 107 | csbeq1d 3369 |
. . . . . . . . . . 11
 
              ![]_ ]_](_urbrack.gif)                                                          ![]_ ]_](_urbrack.gif)                                                          |
109 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . 18
           |
110 | 109 | imaeq2d 5167 |
. . . . . . . . . . . . . . . . 17
                                   |
111 | 110 | xpeq1d 4856 |
. . . . . . . . . . . . . . . 16
                                           |
112 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . 19
       |
113 | 112 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . 18
               |
114 | 113 | imaeq2d 5167 |
. . . . . . . . . . . . . . . . 17
                                       |
115 | 114 | xpeq1d 4856 |
. . . . . . . . . . . . . . . 16
                                               |
116 | 111, 115 | uneq12d 3588 |
. . . . . . . . . . . . . . 15
                                                                                           |
117 | 116 | oveq2d 6304 |
. . . . . . . . . . . . . 14
                                                                                                                 |
118 | 117 | adantl 468 |
. . . . . . . . . . . . 13
 
                                                                                                                 |
119 | 40, 118 | csbied 3389 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)                                                                                                                 |
120 | 119 | adantr 467 |
. . . . . . . . . . 11
 
   ![]_ ]_](_urbrack.gif)                                                                                                                 |
121 | 108, 120 | eqtrd 2484 |
. . . . . . . . . 10
 
              ![]_ ]_](_urbrack.gif)                                                                                                                 |
122 | | ovex 6316 |
. . . . . . . . . . 11
                                                        |
123 | 122 | a1i 11 |
. . . . . . . . . 10
                                                          |
124 | 93, 121, 40, 123 | fvmptd 5952 |
. . . . . . . . 9
                                                              |
125 | 124 | fveq1d 5865 |
. . . . . . . 8
                                                                      |
126 | 125 | adantr 467 |
. . . . . . 7
 
                                                                                        |
127 | | imassrn 5178 |
. . . . . . . . . 10
                           |
128 | | f1of 5812 |
. . . . . . . . . . 11
                    
                      |
129 | | frn 5733 |
. . . . . . . . . . 11
                                   |
130 | 29, 128, 129 | 3syl 18 |
. . . . . . . . . 10
               |
131 | 127, 130 | syl5ss 3442 |
. . . . . . . . 9
                         |
132 | 131 | sselda 3431 |
. . . . . . . 8
 
                         |
133 | | xp1st 6820 |
. . . . . . . . . . 11
        ..^                               ..^        |
134 | | elmapfn 7491 |
. . . . . . . . . . 11
           ..^                    |
135 | 23, 133, 134 | 3syl 18 |
. . . . . . . . . 10
               |
136 | 135 | adantr 467 |
. . . . . . . . 9
 
                                 |
137 | | 1ex 9635 |
. . . . . . . . . . . . . 14
 |
138 | | fnconstg 5769 |
. . . . . . . . . . . . . 14
                                       |
139 | 137, 138 | ax-mp 5 |
. . . . . . . . . . . . 13
                                     |
140 | | c0ex 9634 |
. . . . . . . . . . . . . 14
 |
141 | | fnconstg 5769 |
. . . . . . . . . . . . . 14
                                           |
142 | 140, 141 | ax-mp 5 |
. . . . . . . . . . . . 13
                                         |
143 | 139, 142 | pm3.2i 457 |
. . . . . . . . . . . 12
                                                                               |
144 | | imain 5657 |
. . . . . . . . . . . . . 14
                         
 
                                            |
145 | 29, 36, 144 | 3syl 18 |
. . . . . . . . . . . . 13
                                                               |
146 | 64 | imaeq2d 5167 |
. . . . . . . . . . . . . 14
                                       |
147 | | ima0 5182 |
. . . . . . . . . . . . . 14
             |
148 | 146, 147 | syl6eq 2500 |
. . . . . . . . . . . . 13
                           |
149 | 145, 148 | eqtr3d 2486 |
. . . . . . . . . . . 12
                                       |
150 | | fnun 5680 |
. . . . . . . . . . . 12
                                                                                                                                                                                                       |
151 | 143, 149,
150 | sylancr 668 |
. . . . . . . . . . 11
                                                                                   |
152 | | imaundi 5247 |
. . . . . . . . . . . . 13
                                                             |
153 | 55 | imaeq2d 5167 |
. . . . . . . . . . . . . 14
                                           |
154 | 153, 32 | eqtr3d 2486 |
. . . . . . . . . . . . 13
                               |
155 | 152, 154 | syl5eqr 2498 |
. . . . . . . . . . . 12
                                           |
156 | 155 | fneq2d 5665 |
. . . . . . . . . . 11
                                                                                                                                     |
157 | 151, 156 | mpbid 214 |
. . . . . . . . . 10
                                                   |
158 | 157 | adantr 467 |
. . . . . . . . 9
 
                                                                     |
159 | | ovex 6316 |
. . . . . . . . . 10
     |
160 | 159 | a1i 11 |
. . . . . . . . 9
 
                         |
161 | | inidm 3640 |
. . . . . . . . 9
               |
162 | | eqidd 2451 |
. . . . . . . . 9
                          
                          |
163 | | fvun2 5935 |
. . . . . . . . . . . . 13
                                                                                                                  
                   
                                                                            |
164 | 139, 142,
163 | mp3an12 1353 |
. . . . . . . . . . . 12
                                                                                                                                     |
165 | 149, 164 | sylan 474 |
. . . . . . . . . . 11
 
                                                                                               |
166 | 140 | fvconst2 6118 |
. . . . . . . . . . . 12
                  
                            |
167 | 166 | adantl 468 |
. . . . . . . . . . 11
 
                                               |
168 | 165, 167 | eqtrd 2484 |
. . . . . . . . . 10
 
                                                                     |
169 | 168 | adantr 467 |
. . . . . . . . 9
                          
                                                  |
170 | 136, 158,
160, 160, 161, 162, 169 | ofval 6537 |
. . . . . . . 8
                          
                                                                           |
171 | 132, 170 | mpdan 673 |
. . . . . . 7
 
                                                                                              |
172 | | elmapi 7490 |
. . . . . . . . . . . . 13
           ..^                       ..^   |
173 | 23, 133, 172 | 3syl 18 |
. . . . . . . . . . . 12
                  ..^   |
174 | 173 | ffvelrnda 6020 |
. . . . . . . . . . 11
 
                  ..^   |
175 | | elfzonn0 11957 |
. . . . . . . . . . 11
              ..^               |
176 | 174, 175 | syl 17 |
. . . . . . . . . 10
 
                   |
177 | 176 | nn0cnd 10924 |
. . . . . . . . 9
 
                   |
178 | 177 | addid1d 9830 |
. . . . . . . 8
 
                                 |
179 | 132, 178 | syldan 473 |
. . . . . . 7
 
                                               |
180 | 126, 171,
179 | 3eqtrd 2488 |
. . . . . 6
 
                                         |
181 | 73, 180 | syldan 473 |
. . . . 5
 
                
                 
                      |
182 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . 19
           |
183 | 182 | breq2d 4413 |
. . . . . . . . . . . . . . . . . 18
 
   
       |
184 | 183 | ifbid 3902 |
. . . . . . . . . . . . . . . . 17
                         |
185 | 184 | csbeq1d 3369 |
. . . . . . . . . . . . . . . 16
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
186 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . 19
           |
187 | 186 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . 18
                   |
188 | 186 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
189 | 188 | imaeq1d 5166 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
190 | 189 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . 19
                                           |
191 | 188 | imaeq1d 5166 |
. . . . . . . . . . . . . . . . . . . 20
                                       |
192 | 191 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . 19
                                               |
193 | 190, 192 | uneq12d 3588 |
. . . . . . . . . . . . . . . . . 18
                                                                                           |
194 | 187, 193 | oveq12d 6306 |
. . . . . . . . . . . . . . . . 17
                                                                                                                 |
195 | 194 | csbeq2dv 3780 |
. . . . . . . . . . . . . . . 16
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
196 | 185, 195 | eqtrd 2484 |
. . . . . . . . . . . . . . 15
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
197 | 196 | mpteq2dv 4489 |
. . . . . . . . . . . . . 14
                     ![]_ ]_](_urbrack.gif)                                                                             ![]_ ]_](_urbrack.gif)                                                           |
198 | 197 | eqeq2d 2460 |
. . . . . . . . . . . . 13
 
    
               ![]_ ]_](_urbrack.gif)                                                        
                    ![]_ ]_](_urbrack.gif)                                                            |
199 | 198, 5 | elrab2 3197 |
. . . . . . . . . . . 12

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
200 | 199 | simprbi 466 |
. . . . . . . . . . 11
     
               ![]_ ]_](_urbrack.gif)                                                           |
201 | 3, 200 | syl 17 |
. . . . . . . . . 10
                     ![]_ ]_](_urbrack.gif)                                                           |
202 | | breq1 4404 |
. . . . . . . . . . . . . 14
 
   
       |
203 | 202, 95 | ifbieq1d 3903 |
. . . . . . . . . . . . 13
                         |
204 | | poimirlem12.3 |
. . . . . . . . . . . . . . 15
       |
205 | 103, 204 | breqtrrd 4428 |
. . . . . . . . . . . . . 14
       |
206 | 205 | iftrued 3888 |
. . . . . . . . . . . . 13
              |
207 | 203, 206 | sylan9eqr 2506 |
. . . . . . . . . . . 12
 
              |
208 | 207 | csbeq1d 3369 |
. . . . . . . . . . 11
 
              ![]_ ]_](_urbrack.gif)                                                          ![]_ ]_](_urbrack.gif)                                                          |
209 | 109 | imaeq2d 5167 |
. . . . . . . . . . . . . . . . 17
                                   |
210 | 209 | xpeq1d 4856 |
. . . . . . . . . . . . . . . 16
                                           |
211 | 113 | imaeq2d 5167 |
. . . . . . . . . . . . . . . . 17
                                       |
212 | 211 | xpeq1d 4856 |
. . . . . . . . . . . . . . . 16
                                               |
213 | 210, 212 | uneq12d 3588 |
. . . . . . . . . . . . . . 15
                                                                                           |
214 | 213 | oveq2d 6304 |
. . . . . . . . . . . . . 14
                                                                                                                 |
215 | 214 | adantl 468 |
. . . . . . . . . . . . 13
 
                                                                                                                 |
216 | 40, 215 | csbied 3389 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)                                                                                                                 |
217 | 216 | adantr 467 |
. . . . . . . . . . 11
 
   ![]_ ]_](_urbrack.gif)                                                                                                                 |
218 | 208, 217 | eqtrd 2484 |
. . . . . . . . . 10
 
              ![]_ ]_](_urbrack.gif)                                                                                                                 |
219 | | ovex 6316 |
. . . . . . . . . . 11
                                                        |
220 | 219 | a1i 11 |
. . . . . . . . . 10
                                                          |
221 | 201, 218,
40, 220 | fvmptd 5952 |
. . . . . . . . 9
                                                              |
222 | 221 | fveq1d 5865 |
. . . . . . . 8
                                                                      |
223 | 222 | adantr 467 |
. . . . . . 7
 
                                                                                      |
224 | 18 | sselda 3431 |
. . . . . . . 8
 
                       |
225 | | xp1st 6820 |
. . . . . . . . . . 11
        ..^                               ..^        |
226 | | elmapfn 7491 |
. . . . . . . . . . 11
           ..^                    |
227 | 8, 225, 226 | 3syl 18 |
. . . . . . . . . 10
               |
228 | 227 | adantr 467 |
. . . . . . . . 9
 
                               |
229 | | fnconstg 5769 |
. . . . . . . . . . . . . 14
                                       |
230 | 137, 229 | ax-mp 5 |
. . . . . . . . . . . . 13
                                     |
231 | | fnconstg 5769 |
. . . . . . . . . . . . . 14
                                           |
232 | 140, 231 | ax-mp 5 |
. . . . . . . . . . . . 13
                                         |
233 | 230, 232 | pm3.2i 457 |
. . . . . . . . . . . 12
                                                                               |
234 | | dff1o3 5818 |
. . . . . . . . . . . . . . 15
                                         
            |
235 | 234 | simprbi 466 |
. . . . . . . . . . . . . 14
                    
           |
236 | | imain 5657 |
. . . . . . . . . . . . . 14
                         
 
                                            |
237 | 14, 235, 236 | 3syl 18 |
. . . . . . . . . . . . 13
                                                               |
238 | 64 | imaeq2d 5167 |
. . . . . . . . . . . . . 14
                                       |
239 | | ima0 5182 |
. . . . . . . . . . . . . 14
             |
240 | 238, 239 | syl6eq 2500 |
. . . . . . . . . . . . 13
                           |
241 | 237, 240 | eqtr3d 2486 |
. . . . . . . . . . . 12
                                       |
242 | | fnun 5680 |
. . . . . . . . . . . 12
                                                                                                                                                                                                       |
243 | 233, 241,
242 | sylancr 668 |
. . . . . . . . . . 11
                                                                                   |
244 | | imaundi 5247 |
. . . . . . . . . . . . 13
                                                             |
245 | 55 | imaeq2d 5167 |
. . . . . . . . . . . . . 14
                                           |
246 | | f1ofo 5819 |
. . . . . . . . . . . . . . 15
                    
                      |
247 | | foima 5796 |
. . . . . . . . . . . . . . 15
                                           |
248 | 14, 246, 247 | 3syl 18 |
. . . . . . . . . . . . . 14
                       |
249 | 245, 248 | eqtr3d 2486 |
. . . . . . . . . . . . 13
                               |
250 | 244, 249 | syl5eqr 2498 |
. . . . . . . . . . . 12
                                           |
251 | 250 | fneq2d 5665 |
. . . . . . . . . . 11
                                                                                                                                     |
252 | 243, 251 | mpbid 214 |
. . . . . . . . . 10
                                                   |
253 | 252 | adantr 467 |
. . . . . . . . 9
 
        |