Step | Hyp | Ref
| Expression |
1 | | soseq.1 |
. . . 4

    |
2 | | sopo 4777 |
. . . 4
           |
3 | 1, 2 | ax-mp 5 |
. . 3

    |
4 | | soseq.2 |
. . 3
 
      |
5 | | soseq.3 |
. . 3
   
 
                          |
6 | 3, 4, 5 | poseq 30562 |
. 2
 |
7 | | eleq1 2537 |
. . . . . . . . . . . 12
 
   |
8 | 7 | anbi1d 719 |
. . . . . . . . . . 11
  
      |
9 | | fveq1 5878 |
. . . . . . . . . . . . . . 15
           |
10 | 9 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
         
           |
11 | 10 | ralbidv 2829 |
. . . . . . . . . . . . 13
  
       

           |
12 | | fveq1 5878 |
. . . . . . . . . . . . . 14
           |
13 | 12 | breq1d 4405 |
. . . . . . . . . . . . 13
           
             |
14 | 11, 13 | anbi12d 725 |
. . . . . . . . . . . 12
                        
                      |
15 | 14 | rexbidv 2892 |
. . . . . . . . . . 11
  
                     
                        |
16 | 8, 15 | anbi12d 725 |
. . . . . . . . . 10
     
 
                       
 
                       |
17 | | eleq1 2537 |
. . . . . . . . . . . 12
 
   |
18 | 17 | anbi2d 718 |
. . . . . . . . . . 11
  
      |
19 | | fveq1 5878 |
. . . . . . . . . . . . . . 15
           |
20 | 19 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
         
           |
21 | 20 | ralbidv 2829 |
. . . . . . . . . . . . 13
  
       

           |
22 | | fveq1 5878 |
. . . . . . . . . . . . . 14
           |
23 | 22 | breq2d 4407 |
. . . . . . . . . . . . 13
           
             |
24 | 21, 23 | anbi12d 725 |
. . . . . . . . . . . 12
                        
                      |
25 | 24 | rexbidv 2892 |
. . . . . . . . . . 11
  
                     
                        |
26 | 18, 25 | anbi12d 725 |
. . . . . . . . . 10
     
 
                       
 
                       |
27 | 16, 26, 5 | brabg 4720 |
. . . . . . . . 9
 
       
 
                       |
28 | 27 | bianabs 897 |
. . . . . . . 8
 
    
                        |
29 | | eleq1 2537 |
. . . . . . . . . . . . 13
 
   |
30 | 29 | anbi1d 719 |
. . . . . . . . . . . 12
  
      |
31 | | fveq1 5878 |
. . . . . . . . . . . . . . . 16
           |
32 | 31 | eqeq1d 2473 |
. . . . . . . . . . . . . . 15
         
           |
33 | 32 | ralbidv 2829 |
. . . . . . . . . . . . . 14
  
       

           |
34 | | fveq1 5878 |
. . . . . . . . . . . . . . 15
           |
35 | 34 | breq1d 4405 |
. . . . . . . . . . . . . 14
           
             |
36 | 33, 35 | anbi12d 725 |
. . . . . . . . . . . . 13
                        
                      |
37 | 36 | rexbidv 2892 |
. . . . . . . . . . . 12
  
                     
                        |
38 | 30, 37 | anbi12d 725 |
. . . . . . . . . . 11
     
 
                       
 
                       |
39 | | eleq1 2537 |
. . . . . . . . . . . . 13
 
   |
40 | 39 | anbi2d 718 |
. . . . . . . . . . . 12
  
      |
41 | | fveq1 5878 |
. . . . . . . . . . . . . . . 16
           |
42 | 41 | eqeq2d 2481 |
. . . . . . . . . . . . . . 15
         
           |
43 | 42 | ralbidv 2829 |
. . . . . . . . . . . . . 14
  
       

           |
44 | | fveq1 5878 |
. . . . . . . . . . . . . . 15
           |
45 | 44 | breq2d 4407 |
. . . . . . . . . . . . . 14
           
             |
46 | 43, 45 | anbi12d 725 |
. . . . . . . . . . . . 13
                        
                      |
47 | 46 | rexbidv 2892 |
. . . . . . . . . . . 12
  
                     
                        |
48 | 40, 47 | anbi12d 725 |
. . . . . . . . . . 11
     
 
                       
 
                       |
49 | 38, 48, 5 | brabg 4720 |
. . . . . . . . . 10
 
       
 
                       |
50 | 49 | bianabs 897 |
. . . . . . . . 9
 
    
                        |
51 | 50 | ancoms 460 |
. . . . . . . 8
 
    
                        |
52 | 28, 51 | orbi12d 724 |
. . . . . . 7
 
       
 
 
                     
                       |
53 | 52 | notbid 301 |
. . . . . 6
 
       
 
                       
                       |
54 | | ralinexa 2838 |
. . . . . . . 8
 
 
                              
  
                                 |
55 | | andi 884 |
. . . . . . . . . . 11
                                 
  
                    
                      |
56 | | eqcom 2478 |
. . . . . . . . . . . . . 14
        
          |
57 | 56 | ralbii 2823 |
. . . . . . . . . . . . 13
 
       

          |
58 | 57 | anbi1i 709 |
. . . . . . . . . . . 12
                                             |
59 | 58 | orbi2i 528 |
. . . . . . . . . . 11
                        
                      
                    
                      |
60 | 55, 59 | bitri 257 |
. . . . . . . . . 10
                                 
  
                    
                      |
61 | 60 | rexbii 2881 |
. . . . . . . . 9
   
                              
   
                                           |
62 | | r19.43 2932 |
. . . . . . . . 9
                         
                       
                     
                      |
63 | 61, 62 | bitri 257 |
. . . . . . . 8
   
                              
 
 
                     
                      |
64 | 54, 63 | xchbinx 317 |
. . . . . . 7
 
 
                              
 
                       
                      |
65 | | feq2 5721 |
. . . . . . . . . . . . . . 15
     
       |
66 | 65 | cbvrexv 3006 |
. . . . . . . . . . . . . 14
     
       |
67 | 66 | abbii 2587 |
. . . . . . . . . . . . 13
               |
68 | 4, 67 | eqtri 2493 |
. . . . . . . . . . . 12
 
      |
69 | 68 | orderseqlem 30561 |
. . . . . . . . . . 11
           |
70 | 68 | orderseqlem 30561 |
. . . . . . . . . . 11
           |
71 | | sotrieq 4787 |
. . . . . . . . . . . 12
                                 
                         |
72 | 1, 71 | mpan 684 |
. . . . . . . . . . 11
                           
                         |
73 | 69, 70, 72 | syl2an 485 |
. . . . . . . . . 10
 
                                   |
74 | 73 | imbi2d 323 |
. . . . . . . . 9
 
   
                  
       
                          |
75 | 74 | ralbidv 2829 |
. . . . . . . 8
 
    
                                                      |
76 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
77 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
78 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
79 | 77, 78 | eqeq12d 2486 |
. . . . . . . . . . . . . 14
         
           |
80 | 76, 79 | sbcie 3290 |
. . . . . . . . . . . . 13
   ![]. ].](_drbrack.gif)        
          |
81 | 80 | ralbii 2823 |
. . . . . . . . . . . 12
 
  ![]. ].](_drbrack.gif)                    |
82 | 81 | imbi1i 332 |
. . . . . . . . . . 11
     ![]. ].](_drbrack.gif)                                       |
83 | 82 | ralbii 2823 |
. . . . . . . . . 10
 
 
  ![]. ].](_drbrack.gif)                  
                     |
84 | | tfisg 30528 |
. . . . . . . . . 10
 
 
  ![]. ].](_drbrack.gif)                             |
85 | 83, 84 | sylbir 218 |
. . . . . . . . 9
 
 
                            |
86 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
87 | | feq1 5720 |
. . . . . . . . . . . . . . 15
     
       |
88 | 87 | rexbidv 2892 |
. . . . . . . . . . . . . 14
  
   
        |
89 | 86, 88, 4 | elab2 3176 |
. . . . . . . . . . . . 13

       |
90 | | feq2 5721 |
. . . . . . . . . . . . . 14
     
       |
91 | 90 | cbvrexv 3006 |
. . . . . . . . . . . . 13
     
       |
92 | 89, 91 | bitri 257 |
. . . . . . . . . . . 12

       |
93 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
94 | | feq1 5720 |
. . . . . . . . . . . . . . 15
     
       |
95 | 94 | rexbidv 2892 |
. . . . . . . . . . . . . 14
  
   
        |
96 | 93, 95, 4 | elab2 3176 |
. . . . . . . . . . . . 13

       |
97 | | feq2 5721 |
. . . . . . . . . . . . . 14
     
       |
98 | 97 | cbvrexv 3006 |
. . . . . . . . . . . . 13
     
       |
99 | 96, 98 | bitri 257 |
. . . . . . . . . . . 12

       |
100 | 92, 99 | anbi12i 711 |
. . . . . . . . . . 11
 
               |
101 | | reeanv 2944 |
. . . . . . . . . . 11
  
                        |
102 | 100, 101 | bitr4i 260 |
. . . . . . . . . 10
 
  
            |
103 | | onss 6636 |
. . . . . . . . . . . . . . . . . . 19
   |
104 | | ssralv 3479 |
. . . . . . . . . . . . . . . . . . 19

 
        
           |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . 18
  
        
           |
106 | 105 | ad2antlr 741 |
. . . . . . . . . . . . . . . . 17
              
 
        
           |
107 | | soseq.4 |
. . . . . . . . . . . . . . . . . . 19
 |
108 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
109 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
110 | 108, 109 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
           |
111 | 110 | rspcv 3132 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
                   |
112 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
              

 
                    |
113 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
      |
114 | | fdm 5745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
  |
115 | | eloni 5440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
116 | | ordirr 5448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
118 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
119 | 118 | notbid 301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
   |
120 | 119 | biimparc 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  
  |
121 | 117, 120 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

  |
122 | | ndmfv 5903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
123 | | eqtr2 2491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                     |
124 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
       |
125 | 124 | biimprd 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
126 | 123, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                   
   |
127 | 126 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
                  |
128 | 121, 122,
127 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

                  |
129 | 128 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

    
             |
130 | 114, 129 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
             |
131 | 130 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                           |
132 | 113, 131 | syl5 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                             |
133 | 132 | exp4b 618 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     
              
      |
134 | 133 | imp32 440 |
. . . . . . . . . . . . . . . . . . . . . 22
              

             |
135 | 112, 134 | syldd 67 |
. . . . . . . . . . . . . . . . . . . . 21
              

 
            |
136 | 135 | com23 80 |
. . . . . . . . . . . . . . . . . . . 20
              
 
             |
137 | 136 | imp 436 |
. . . . . . . . . . . . . . . . . . 19
                
        

   |
138 | 107, 137 | mtoi 183 |
. . . . . . . . . . . . . . . . . 18
                
        
  |
139 | 138 | ex 441 |
. . . . . . . . . . . . . . . . 17
              
 
       
   |
140 | 106, 139 | syld 44 |
. . . . . . . . . . . . . . . 16
              
 
       
   |
141 | | onss 6636 |
. . . . . . . . . . . . . . . . . . 19
   |
142 | | ssralv 3479 |
. . . . . . . . . . . . . . . . . . 19

 
        
           |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . 18
  
        
           |
144 | 143 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
              
 
        
           |
145 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
146 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
147 | 145, 146 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
           |
148 | 147 | rspcv 3132 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
                   |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
              

 
                    |
150 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
       |
151 | | fdm 5745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
  |
152 | | eloni 5440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
153 | | ordirr 5448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
155 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     |
156 | 155 | notbid 301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   |
157 | 156 | biimparc 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  
  |
158 | | ndmfv 5903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         |
160 | 154, 159 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

      |
161 | | eqtr 2490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                     |
162 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
    
   |
163 | 162 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
        |
164 | 161, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                   
   |
165 | 164 | expcom 442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
                  |
166 | 165 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
                  |
167 | 160, 166 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

    
             |
168 | 167 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                       |
169 | 151, 168 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                           |
170 | 150, 169 | syl5 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                             |
171 | 170 | exp4b 618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     
                     |
172 | 171 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     
                     |
173 | 172 | imp32 440 |
. . . . . . . . . . . . . . . . . . . . . 22
              

             |
174 | 149, 173 | syldd 67 |
. . . . . . . . . . . . . . . . . . . . 21
              

 
            |
175 | 174 | com23 80 |
. . . . . . . . . . . . . . . . . . . 20
              
 
             |
176 | 175 | imp 436 |
. . . . . . . . . . . . . . . . . . 19
                
        

   |
177 | 107, 176 | mtoi 183 |
. . . . . . . . . . . . . . . . . 18
                
        
  |
178 | 177 | ex 441 |
. . . . . . . . . . . . . . . . 17
              
 
       
   |
179 | 144, 178 | syld 44 |
. . . . . . . . . . . . . . . 16
              
 
       
   |
180 | 140, 179 | jcad 542 |
. . . . . . . . . . . . . . 15
              
 
        
    |
181 | | ordtri3or 5462 |
. . . . . . . . . . . . . . . . 17
       |
182 | 115, 152,
181 | syl2an 485 |
. . . . . . . . . . . . . . . 16
 
     |
183 | 182 | adantr 472 |
. . . . . . . . . . . . . . 15
              

   |
184 | | 3orel13 30421 |
. . . . . . . . . . . . . . 15
     
   |
185 | 180, 183,
184 | syl6ci 66 |
. . . . . . . . . . . . . 14
              
 
           |
186 | 185, 144 | jcad 542 |
. . . . . . . . . . . . 13
              
 
                      |
187 | | ffn 5739 |
. . . . . . . . . . . . . . 15
       |
188 | | ffn 5739 |
. . . . . . . . . . . . . . 15
       |
189 | | eqfnfv2 5992 |
. . . . . . . . . . . . . . 15
 
                |
190 | 187, 188,
189 | syl2an 485 |
. . . . . . . . . . . . . 14
             
            |
191 | 190 | adantl 473 |
. . . . . . . . . . . . 13
              

 
            |
192 | 186, 191 | sylibrd 242 |
. . . . . . . . . . . 12
              
 
           |
193 | 192 | ex 441 |
. . . . . . . . . . 11
 
                          |
194 | 193 | rexlimivv 2876 |
. . . . . . . . . 10
  
                       |
195 | 102, 194 | sylbi 200 |
. . . . . . . . 9
 
              |
196 | 85, 195 | syl5 32 |
. . . . . . . 8
 
    
                
   |
197 | 75, 196 | sylbird 243 |
. . . . . . 7
 
    
       
                          |
198 | 64, 197 | syl5bir 226 |
. . . . . 6
 
     
                     
                       |
199 | 53, 198 | sylbid 223 |
. . . . 5
 
           |
200 | 199 | orrd 385 |
. . . 4
 
           |
201 | | 3orcomb 1017 |
. . . . 5
               |
202 | | df-3or 1008 |
. . . . 5
                 |
203 | 201, 202 | bitr2i 258 |
. . . 4
        
  
     |
204 | 200, 203 | sylib 201 |
. . 3
 
         |
205 | 204 | rgen2a 2820 |
. 2


  
    |
206 | | df-so 4761 |
. 2




  
      |
207 | 6, 205, 206 | mpbir2an 934 |
1
 |