Proof of Theorem poimirlem22
Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . 5
   |
2 | 1 | adantr 467 |
. . . 4
 
          
  |
3 | | poimirlem22.s |
. . . 4
     ..^                                              ![]_ ]_](_urbrack.gif)                                                           |
4 | | poimirlem22.1 |
. . . . 5
               
       |
5 | 4 | adantr 467 |
. . . 4
 
          
     
                |
6 | | poimirlem22.2 |
. . . . 5
   |
7 | 6 | adantr 467 |
. . . 4
 
          
  |
8 | | simpr 463 |
. . . 4
 
          
            |
9 | 2, 3, 5, 7, 8 | poimirlem15 31948 |
. . 3
 
          
                                                                         
       |
10 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
11 | 10 | breq2d 4413 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   
       |
12 | 11 | ifbid 3902 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
13 | 12 | csbeq1d 3369 |
. . . . . . . . . . . . . . . . . . . . 21
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
14 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
15 | 14 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
16 | 14 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
17 | 16 | imaeq1d 5166 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                   |
18 | 17 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                           |
19 | 16 | imaeq1d 5166 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                       |
20 | 19 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                               |
21 | 18, 20 | uneq12d 3588 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                                           |
22 | 15, 21 | oveq12d 6306 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                                                                                 |
23 | 22 | csbeq2dv 3780 |
. . . . . . . . . . . . . . . . . . . . 21
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
24 | 13, 23 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . 20
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
25 | 24 | mpteq2dv 4489 |
. . . . . . . . . . . . . . . . . . 19
                     ![]_ ]_](_urbrack.gif)                                                                             ![]_ ]_](_urbrack.gif)                                                           |
26 | 25 | eqeq2d 2460 |
. . . . . . . . . . . . . . . . . 18
 
    
               ![]_ ]_](_urbrack.gif)                                                        
                    ![]_ ]_](_urbrack.gif)                                                            |
27 | 26, 3 | elrab2 3197 |
. . . . . . . . . . . . . . . . 17

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
28 | 27 | simprbi 466 |
. . . . . . . . . . . . . . . 16
     
               ![]_ ]_](_urbrack.gif)                                                           |
29 | 6, 28 | syl 17 |
. . . . . . . . . . . . . . 15
                     ![]_ ]_](_urbrack.gif)                                                           |
30 | 29 | adantr 467 |
. . . . . . . . . . . . . 14
 
          
                    ![]_ ]_](_urbrack.gif)                                                           |
31 | | elrabi 3192 |
. . . . . . . . . . . . . . . . . . . . 21
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
32 | 31, 3 | eleq2s 2546 |
. . . . . . . . . . . . . . . . . . . 20
     ..^                            |
33 | 6, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     ..^                            |
34 | | xp1st 6820 |
. . . . . . . . . . . . . . . . . . 19
     ..^                                 ..^                       |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . 18
        ..^                       |
36 | | xp1st 6820 |
. . . . . . . . . . . . . . . . . 18
        ..^                               ..^        |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
           ..^        |
38 | | elmapi 7490 |
. . . . . . . . . . . . . . . . 17
           ..^                       ..^   |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
                  ..^   |
40 | | elfzoelz 11917 |
. . . . . . . . . . . . . . . . 17
  ..^
  |
41 | 40 | ssriv 3435 |
. . . . . . . . . . . . . . . 16
 ..^  |
42 | | fss 5735 |
. . . . . . . . . . . . . . . 16
                   ..^  ..^ 
                  |
43 | 39, 41, 42 | sylancl 667 |
. . . . . . . . . . . . . . 15
                   |
44 | 43 | adantr 467 |
. . . . . . . . . . . . . 14
 
          
                  |
45 | | xp2nd 6821 |
. . . . . . . . . . . . . . . . 17
        ..^                                             |
46 | 35, 45 | syl 17 |
. . . . . . . . . . . . . . . 16
                         |
47 | | fvex 5873 |
. . . . . . . . . . . . . . . . 17
         |
48 | | f1oeq1 5803 |
. . . . . . . . . . . . . . . . 17
                                             |
49 | 47, 48 | elab 3184 |
. . . . . . . . . . . . . . . 16
                      
                      |
50 | 46, 49 | sylib 200 |
. . . . . . . . . . . . . . 15
                       |
51 | 50 | adantr 467 |
. . . . . . . . . . . . . 14
 
          
                      |
52 | 2, 30, 44, 51, 8 | poimirlem1 31934 |
. . . . . . . . . . . . 13
 
          
                                  |
53 | 52 | adantr 467 |
. . . . . . . . . . . 12
          
    
                                 |
54 | 1 | ad3antrrr 735 |
. . . . . . . . . . . . . . 15
              
         
  |
55 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
56 | 55 | breq2d 4413 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   
       |
57 | 56 | ifbid 3902 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
58 | 57 | csbeq1d 3369 |
. . . . . . . . . . . . . . . . . . . . 21
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
59 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
60 | 59 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
61 | 59 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
62 | 61 | imaeq1d 5166 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                   |
63 | 62 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                           |
64 | 61 | imaeq1d 5166 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                       |
65 | 64 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                               |
66 | 63, 65 | uneq12d 3588 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                                           |
67 | 60, 66 | oveq12d 6306 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                                                                                 |
68 | 67 | csbeq2dv 3780 |
. . . . . . . . . . . . . . . . . . . . 21
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
69 | 58, 68 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . 20
              ![]_ ]_](_urbrack.gif)                                                                     ![]_ ]_](_urbrack.gif)                                                          |
70 | 69 | mpteq2dv 4489 |
. . . . . . . . . . . . . . . . . . 19
                     ![]_ ]_](_urbrack.gif)                                                                             ![]_ ]_](_urbrack.gif)                                                           |
71 | 70 | eqeq2d 2460 |
. . . . . . . . . . . . . . . . . 18
 
    
               ![]_ ]_](_urbrack.gif)                                                        
                    ![]_ ]_](_urbrack.gif)                                                            |
72 | 71, 3 | elrab2 3197 |
. . . . . . . . . . . . . . . . 17

     ..^                              
               ![]_ ]_](_urbrack.gif)                                                            |
73 | 72 | simprbi 466 |
. . . . . . . . . . . . . . . 16
     
               ![]_ ]_](_urbrack.gif)                                                           |
74 | 73 | ad2antlr 732 |
. . . . . . . . . . . . . . 15
              
         
    
               ![]_ ]_](_urbrack.gif)                                                           |
75 | | elrabi 3192 |
. . . . . . . . . . . . . . . . . . . . 21
      ..^                              
               ![]_ ]_](_urbrack.gif)                                                              ..^                            |
76 | 75, 3 | eleq2s 2546 |
. . . . . . . . . . . . . . . . . . . 20
     ..^                            |
77 | | xp1st 6820 |
. . . . . . . . . . . . . . . . . . . 20
     ..^                                 ..^                       |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
        ..^                       |
79 | | xp1st 6820 |
. . . . . . . . . . . . . . . . . . 19
        ..^                               ..^        |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . . 18
           ..^        |
81 | | elmapi 7490 |
. . . . . . . . . . . . . . . . . 18
           ..^                       ..^   |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . 17
                  ..^   |
83 | | fss 5735 |
. . . . . . . . . . . . . . . . 17
                   ..^  ..^ 
                  |
84 | 82, 41, 83 | sylancl 667 |
. . . . . . . . . . . . . . . 16
                   |
85 | 84 | ad2antlr 732 |
. . . . . . . . . . . . . . 15
              
                            |
86 | | xp2nd 6821 |
. . . . . . . . . . . . . . . . . 18
        ..^                                             |
87 | 78, 86 | syl 17 |
. . . . . . . . . . . . . . . . 17
                         |
88 | | fvex 5873 |
. . . . . . . . . . . . . . . . . 18
         |
89 | | f1oeq1 5803 |
. . . . . . . . . . . . . . . . . 18
                                             |
90 | 88, 89 | elab 3184 |
. . . . . . . . . . . . . . . . 17
                      
                      |
91 | 87, 90 | sylib 200 |
. . . . . . . . . . . . . . . 16
                       |
92 | 91 | ad2antlr 732 |
. . . . . . . . . . . . . . 15
              
                                |
93 | | simpllr 768 |
. . . . . . . . . . . . . . 15
              
                      |
94 | | xp2nd 6821 |
. . . . . . . . . . . . . . . . . 18
     ..^                                    |
95 | 76, 94 | syl 17 |
. . . . . . . . . . . . . . . . 17
           |
96 | 95 | adantl 468 |
. . . . . . . . . . . . . . . 16
          
              |
97 | | eldifsn 4096 |
. . . . . . . . . . . . . . . . 17
                
        
           |
98 | 97 | biimpri 210 |
. . . . . . . . . . . . . . . 16
                                     |
99 | 96, 98 | sylan 474 |
. . . . . . . . . . . . . . 15
              
                            |
100 | 54, 74, 85, 92, 93, 99 | poimirlem2 31935 |
. . . . . . . . . . . . . 14
              
          
                                 |
101 | 100 | ex 436 |
. . . . . . . . . . . . 13
          
             
                                  |
102 | 101 | necon1bd 2641 |
. . . . . . . . . . . 12
          
                                    
           |
103 | 53, 102 | mpd 15 |
. . . . . . . . . . 11
          
              |
104 | | eleq1 2516 |
. . . . . . . . . . . . . . . 16
        
        
               |
105 | 104 | biimparc 490 |
. . . . . . . . . . . . . . 15
                            
    |
106 | 105 | anim2i 572 |
. . . . . . . . . . . . . 14
 
        
                          |
107 | 106 | anassrs 653 |
. . . . . . . . . . . . 13
          
                          |
108 | 73 | adantl 468 |
. . . . . . . . . . . . . 14
          
        
               ![]_ ]_](_urbrack.gif)                                                           |
109 | | breq1 4404 |
. . . . . . . . . . . . . . . . . 18
 
   
       |
110 | | id 22 |
. . . . . . . . . . . . . . . . . 18
   |
111 | 109, 110 | ifbieq1d 3903 |
. . . . . . . . . . . . . . . . 17
                         |
112 | | elfznn 11825 |
. . . . . . . . . . . . . . . . . . . 20
                 |
113 | 112 | nngt0d 10650 |
. . . . . . . . . . . . . . . . . . 19
                 |
114 | 113 | iftrued 3888 |
. . . . . . . . . . . . . . . . . 18
                        |
115 | 114 | ad2antlr 732 |
. . . . . . . . . . . . . . . . 17
          
                 |
116 | 111, 115 | sylan9eqr 2506 |
. . . . . . . . . . . . . . . 16
              


 
           |
117 | 116 | csbeq1d 3369 |
. . . . . . . . . . . . . . 15
              


             ![]_ ]_](_urbrack.gif)                                                          ![]_ ]_](_urbrack.gif)                                                          |
118 | | c0ex 9634 |
. . . . . . . . . . . . . . . . . 18
 |
119 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
120 | | fz10 11817 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
121 | 119, 120 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
122 | 121 | imaeq2d 5167 |
. . . . . . . . . . . . . . . . . . . . . 22
                               |
123 | 122 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . . . 21
                                       |
124 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
125 | | 0p1e1 10718 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
126 | 124, 125 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
127 | 126 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
128 | 127 | imaeq2d 5167 |
. . . . . . . . . . . . . . . . . . . . . 22
                                     |
129 | 128 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . . . 21
                                             |
130 | 123, 129 | uneq12d 3588 |
. . . . . . . . . . . . . . . . . . . 20
                                                                                     |
131 | | ima0 5182 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
132 | 131 | xpeq1i 4853 |
. . . . . . . . . . . . . . . . . . . . . . 23
                
    |
133 | | 0xp 4914 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
134 | 132, 133 | eqtri 2472 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
135 | 134 | uneq1i 3583 |
. . . . . . . . . . . . . . . . . . . . 21
                                      
                      |
136 | | uncom 3577 |
. . . . . . . . . . . . . . . . . . . . 21
                                             |
137 | | un0 3758 |
. . . . . . . . . . . . . . . . . . . . 21
                                           |
138 | 135, 136,
137 | 3eqtri 2476 |
. . . . . . . . . . . . . . . . . . . 20
                                                           |
139 | 130, 138 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . 19
                                                                   |
140 | 139 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . 18
                                                                                         |
141 | 118, 140 | csbie 3388 |
. . . . . . . . . . . . . . . . 17
  ![]_ ]_](_urbrack.gif)                                                                                        |
142 | | f1ofo 5819 |
. . . . . . . . . . . . . . . . . . . . . 22
                    
                      |
143 | 91, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
144 | | foima 5796 |
. . . . . . . . . . . . . . . . . . . . 21
                                           |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                       |
146 | 145 | xpeq1d 4856 |
. . . . . . . . . . . . . . . . . . 19
                               |
147 | 146 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . 18
                                                     |
148 | | ovex 6316 |
. . . . . . . . . . . . . . . . . . . 20
     |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
       |
150 | | ffn 5726 |
. . . . . . . . . . . . . . . . . . . 20
                  ..^
              |
151 | 82, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
               |
152 | | fnconstg 5769 |
. . . . . . . . . . . . . . . . . . . 20
               |
153 | 118, 152 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
               |
154 | | eqidd 2451 |
. . . . . . . . . . . . . . . . . . 19
 
                               |
155 | 118 | fvconst2 6118 |
. . . . . . . . . . . . . . . . . . . 20
                   |
156 | 155 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 
                   |
157 | 82 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                  ..^   |
158 | | elfzonn0 11957 |
. . . . . . . . . . . . . . . . . . . . . 22
              ..^               |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
                   |
160 | 159 | nn0cnd 10924 |
. . . . . . . . . . . . . . . . . . . 20
 
                   |
161 | 160 | addid1d 9830 |
. . . . . . . . . . . . . . . . . . 19
 
                                 |
162 | 149, 151,
153, 151, 154, 156, 161 | offveq 6549 |
. . . . . . . . . . . . . . . . . 18
                              |
163 | 147, 162 | eqtrd 2484 |
. . . . . . . . . . . . . . . . 17
                                          |
164 | 141, 163 | syl5eq 2496 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)                                                                  |
165 | 164 | ad2antlr 732 |
. . . . . . . . . . . . . . 15
              


  ![]_ ]_](_urbrack.gif)                                                                  |
166 | 117, 165 | eqtrd 2484 |
. . . . . . . . . . . . . 14
              


             ![]_ ]_](_urbrack.gif)                                                                  |
167 | | nnm1nn0 10908 |
. . . . . . . . . . . . . . . . 17
 
   |
168 | 1, 167 | syl 17 |
. . . . . . . . . . . . . . . 16
     |
169 | | 0elfz 11886 |
. . . . . . . . . . . . . . . 16
  
   
    |
170 | 168, 169 | syl 17 |
. . . . . . . . . . . . . . 15
         |
171 | 170 | ad2antrr 731 |
. . . . . . . . . . . . . 14
          
       
    |
172 | | fvex 5873 |
. . . . . . . . . . . . . . 15
         |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . 14
          
              |
174 | 108, 166,
171, 173 | fvmptd 5952 |
. . . . . . . . . . . . 13
          
                  |
175 | 107, 174 | sylan 474 |
. . . . . . . . . . . 12
                                       |
176 | 175 | an32s 812 |
. . . . . . . . . . 11
              
                        |
177 | 103, 176 | mpdan 673 |
. . . . . . . . . 10
          
                  |
178 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
           |
179 | 178 | eleq1d 2512 |
. . . . . . . . . . . . . . 15
           
             |
180 | 179 | anbi2d 709 |
. . . . . . . . . . . . . 14
  
       
  
               |
181 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
           |
182 | 181 | fveq2d 5867 |
. . . . . . . . . . . . . . 15
                   |
183 | 182 | eqeq2d 2460 |
. . . . . . . . . . . . . 14
             
               |
184 | 180, 183 | imbi12d 322 |
. . . . . . . . . . . . 13
                           
                             |
185 | 174 | expcom 437 |
. . . . . . . . . . . . 13
  
       
                  |
186 | 184, 185 | vtoclga 3112 |
. . . . . . . . . . . 12
  
       
                  |
187 | 7, 186 | mpcom 37 |
. . . . . . . . . . 11
 
          
              |
188 | 187 | adantr 467 |
. . . . . . . . . 10
          
                  |
189 | 177, 188 | eqtr3d 2486 |
. . . . . . . . 9
          
                      |
190 | 189 | adantr 467 |
. . . . . . . 8
              


                  |
191 | 1 | ad3antrrr 735 |
. . . . . . . . 9
              


  |
192 | 6 | ad3antrrr 735 |
. . . . . . . . 9
              


  |
193 | | simpllr 768 |
. . . . . . . . 9
              


            |
194 | | simplr 761 |
. . . . . . . . 9
              


  |
195 | 35 | adantr 467 |
. . . . . . . . . . . . . 14
 
          
       ..^                       |
196 | | xpopth 6829 |
. . . . . . . . . . . . . 14
         ..^                            ..^                                                                    |
197 | 78, 195, 196 | syl2anr 481 |
. . . . . . . . . . . . 13
          
                                                  |
198 | 33 | adantr 467 |
. . . . . . . . . . . . . . 15
 
          
    ..^                            |
199 | | xpopth 6829 |
. . . . . . . . . . . . . . . 16
      ..^                              ..^                          
                  
   |
200 | 199 | biimpd 211 |
. . . . . . . . . . . . . . 15
      ..^                              ..^                          
                      |
201 | 76, 198, 200 | syl2anr 481 |
. . . . . . . . . . . . . 14
          
                          |
202 | 103, 201 | mpan2d 679 |
. . . . . . . . . . . . 13
          
                |
203 | 197, 202 | sylbid 219 |
. . . . . . . . . . . 12
          
                                      
   |
204 | 189, 203 | mpand 680 |
. . . . . . . . . . 11
          
                        |
205 | 204 | necon3d 2644 |
. . . . . . . . . 10
          
                        |
206 | 205 | imp 431 |
. . . . . . . . 9
              


                  |
207 | 191, 3, 192, 193, 194, 206 | poimirlem9 31942 |
. . . . . . . 8
              


                                                                       |
208 | 103 | adantr 467 |
. . . . . . . 8
              


          |
209 | 190, 207,
208 | jca31 537 |
. . . . . . 7
              


                                                                
                                  |
210 | 209 | ex 436 |
. . . . . 6
          
                                                                                                         |
211 | | simplr 761 |
. . . . . . . 8
                                                                 
                                                                                                       |
212 | | elfznn 11825 |
. . . . . . . . . . . . . 14
                 |
213 | 212 | nnred 10621 |
. . . . . . . . . . . . 13
                 |
214 | 213 | ltp1d 10534 |
. . . . . . . . . . . . 13
                       |
215 | 213, 214 | ltned 9768 |
. . . . . . . . . . . 12
                       |
216 | 215 | adantl 468 |
. . . . . . . . . . 11
 
          
            |
217 | | fveq1 5862 |
. . . . . . . . . . . . 13
                                                                                                               
                                             |
218 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
219 | | ltp1 10440 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
220 | 218, 219 | ltned 9768 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
221 | | fvex 5873 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
222 | | ovex 6316 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
223 | 221, 222,
222, 221 | fpr 6070 |
. . . . . . . . . . . . . . . . . . . . 21
          
              
                                              |
224 | 220, 223 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                                                                  |
225 | | f1oi 5848 |
. . . . . . . . . . . . . . . . . . . . 21
                          
                                    |
226 | | f1of 5812 |
. . . . . . . . . . . . . . . . . . . . 21

                          
                                  
                          
                                     |
227 | 225, 226 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
                          
                                    |
228 | | disjdif 3838 |
. . . . . . . . . . . . . . . . . . . . 21
                                   |
229 | | fun 5744 |
. . . . . . . . . . . . . . . . . . . . 21
                 
                                           
                                                                                                                                                                                                                               |
230 | 228, 229 | mpan2 676 |
. . . . . . . . . . . . . . . . . . . 20
                                                            
                                                                                            
                                         
                                                     |
231 | 224, 227,
230 | sylancl 667 |
. . . . . . . . . . . . . . . . . . 19
                                  
                                         
                                                     |
232 | 221 | prid1 4079 |
. . . . . . . . . . . . . . . . . . . 20
                  |
233 | | elun1 3600 |
. . . . . . . . . . . . . . . . . . . 20
                 
                                        |
234 | 232, 233 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
                                       |
235 | | fvco3 5940 |
. . . . . . . . . . . . . . . . . . 19
                 
                                                                                                                                                                           
                                                                                    
                               |
236 | 231, 234,
235 | sylancl 667 |
. . . . . . . . . . . . . . . . . 18
                                                                                                                   
                               |
237 | | ffn 5726 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                                                                        |
238 | 224, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
                                                 |
239 | | fnresi 5691 |
. . . . . . . . . . . . . . . . . . . . . 22
                        
               |
240 | 228, 232 | pm3.2i 457 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                      |
241 | | fvun1 5934 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                
                                                                                                                      
                 |