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

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

    |
4 | | soseq.2 |
. . 3
 
      |
5 | | soseq.3 |
. . 3
   
 
                          |
6 | 3, 4, 5 | poseq 27859 |
. 2
 |
7 | | eleq1 2526 |
. . . . . . . . . . . 12
 
   |
8 | 7 | anbi1d 704 |
. . . . . . . . . . 11
  
      |
9 | | fveq1 5799 |
. . . . . . . . . . . . . . 15
           |
10 | 9 | eqeq1d 2456 |
. . . . . . . . . . . . . 14
         
           |
11 | 10 | ralbidv 2846 |
. . . . . . . . . . . . 13
  
       

           |
12 | | fveq1 5799 |
. . . . . . . . . . . . . 14
           |
13 | 12 | breq1d 4411 |
. . . . . . . . . . . . 13
           
             |
14 | 11, 13 | anbi12d 710 |
. . . . . . . . . . . 12
                        
                      |
15 | 14 | rexbidv 2868 |
. . . . . . . . . . 11
  
                     
                        |
16 | 8, 15 | anbi12d 710 |
. . . . . . . . . 10
     
 
                       
 
                       |
17 | | eleq1 2526 |
. . . . . . . . . . . 12
 
   |
18 | 17 | anbi2d 703 |
. . . . . . . . . . 11
  
      |
19 | | fveq1 5799 |
. . . . . . . . . . . . . . 15
           |
20 | 19 | eqeq2d 2468 |
. . . . . . . . . . . . . 14
         
           |
21 | 20 | ralbidv 2846 |
. . . . . . . . . . . . 13
  
       

           |
22 | | fveq1 5799 |
. . . . . . . . . . . . . 14
           |
23 | 22 | breq2d 4413 |
. . . . . . . . . . . . 13
           
             |
24 | 21, 23 | anbi12d 710 |
. . . . . . . . . . . 12
                        
                      |
25 | 24 | rexbidv 2868 |
. . . . . . . . . . 11
  
                     
                        |
26 | 18, 25 | anbi12d 710 |
. . . . . . . . . 10
     
 
                       
 
                       |
27 | 16, 26, 5 | brabg 4717 |
. . . . . . . . 9
 
       
 
                       |
28 | 27 | bianabs 875 |
. . . . . . . 8
 
    
                        |
29 | | eleq1 2526 |
. . . . . . . . . . . . 13
 
   |
30 | 29 | anbi1d 704 |
. . . . . . . . . . . 12
  
      |
31 | | fveq1 5799 |
. . . . . . . . . . . . . . . 16
           |
32 | 31 | eqeq1d 2456 |
. . . . . . . . . . . . . . 15
         
           |
33 | 32 | ralbidv 2846 |
. . . . . . . . . . . . . 14
  
       

           |
34 | | fveq1 5799 |
. . . . . . . . . . . . . . 15
           |
35 | 34 | breq1d 4411 |
. . . . . . . . . . . . . 14
           
             |
36 | 33, 35 | anbi12d 710 |
. . . . . . . . . . . . 13
                        
                      |
37 | 36 | rexbidv 2868 |
. . . . . . . . . . . 12
  
                     
                        |
38 | 30, 37 | anbi12d 710 |
. . . . . . . . . . 11
     
 
                       
 
                       |
39 | | eleq1 2526 |
. . . . . . . . . . . . 13
 
   |
40 | 39 | anbi2d 703 |
. . . . . . . . . . . 12
  
      |
41 | | fveq1 5799 |
. . . . . . . . . . . . . . . 16
           |
42 | 41 | eqeq2d 2468 |
. . . . . . . . . . . . . . 15
         
           |
43 | 42 | ralbidv 2846 |
. . . . . . . . . . . . . 14
  
       

           |
44 | | fveq1 5799 |
. . . . . . . . . . . . . . 15
           |
45 | 44 | breq2d 4413 |
. . . . . . . . . . . . . 14
           
             |
46 | 43, 45 | anbi12d 710 |
. . . . . . . . . . . . 13
                        
                      |
47 | 46 | rexbidv 2868 |
. . . . . . . . . . . 12
  
                     
                        |
48 | 40, 47 | anbi12d 710 |
. . . . . . . . . . 11
     
 
                       
 
                       |
49 | 38, 48, 5 | brabg 4717 |
. . . . . . . . . 10
 
       
 
                       |
50 | 49 | bianabs 875 |
. . . . . . . . 9
 
    
                        |
51 | 50 | ancoms 453 |
. . . . . . . 8
 
    
                        |
52 | 28, 51 | orbi12d 709 |
. . . . . . 7
 
       
 
 
                     
                       |
53 | 52 | notbid 294 |
. . . . . 6
 
       
 
                       
                       |
54 | | ralinexa 2882 |
. . . . . . . 8
 
 
                              
  
                                 |
55 | | andi 862 |
. . . . . . . . . . 11
                                 
  
                    
                      |
56 | | eqcom 2463 |
. . . . . . . . . . . . . 14
        
          |
57 | 56 | ralbii 2839 |
. . . . . . . . . . . . 13
 
       

          |
58 | 57 | anbi1i 695 |
. . . . . . . . . . . 12
                                             |
59 | 58 | orbi2i 519 |
. . . . . . . . . . 11
                        
                      
                    
                      |
60 | 55, 59 | bitri 249 |
. . . . . . . . . 10
                                 
  
                    
                      |
61 | 60 | rexbii 2862 |
. . . . . . . . 9
   
                              
   
                                           |
62 | | r19.43 2982 |
. . . . . . . . 9
                         
                       
                     
                      |
63 | 61, 62 | bitri 249 |
. . . . . . . 8
   
                              
 
 
                     
                      |
64 | 54, 63 | xchbinx 310 |
. . . . . . 7
 
 
                              
 
                       
                      |
65 | | feq2 5652 |
. . . . . . . . . . . . . . 15
     
       |
66 | 65 | cbvrexv 3054 |
. . . . . . . . . . . . . 14
     
       |
67 | 66 | abbii 2588 |
. . . . . . . . . . . . 13
               |
68 | 4, 67 | eqtri 2483 |
. . . . . . . . . . . 12
 
      |
69 | 68 | orderseqlem 27858 |
. . . . . . . . . . 11
           |
70 | 68 | orderseqlem 27858 |
. . . . . . . . . . 11
           |
71 | | sotrieq 4777 |
. . . . . . . . . . . 12
                                 
                         |
72 | 1, 71 | mpan 670 |
. . . . . . . . . . 11
                           
                         |
73 | 69, 70, 72 | syl2an 477 |
. . . . . . . . . 10
 
                                   |
74 | 73 | imbi2d 316 |
. . . . . . . . 9
 
   
                  
       
                          |
75 | 74 | ralbidv 2846 |
. . . . . . . 8
 
    
                                                      |
76 | | vex 3081 |
. . . . . . . . . . . . . 14
 |
77 | | fveq2 5800 |
. . . . . . . . . . . . . . 15
           |
78 | | fveq2 5800 |
. . . . . . . . . . . . . . 15
           |
79 | 77, 78 | eqeq12d 2476 |
. . . . . . . . . . . . . 14
         
           |
80 | 76, 79 | sbcie 3329 |
. . . . . . . . . . . . 13
   ![]. ].](_drbrack.gif)        
          |
81 | 80 | ralbii 2839 |
. . . . . . . . . . . 12
 
  ![]. ].](_drbrack.gif)                    |
82 | 81 | imbi1i 325 |
. . . . . . . . . . 11
     ![]. ].](_drbrack.gif)                                       |
83 | 82 | ralbii 2839 |
. . . . . . . . . 10
 
 
  ![]. ].](_drbrack.gif)                  
                     |
84 | | tfisg 27810 |
. . . . . . . . . 10
 
 
  ![]. ].](_drbrack.gif)                             |
85 | 83, 84 | sylbir 213 |
. . . . . . . . 9
 
 
                            |
86 | | vex 3081 |
. . . . . . . . . . . . . 14
 |
87 | | feq1 5651 |
. . . . . . . . . . . . . . 15
     
       |
88 | 87 | rexbidv 2868 |
. . . . . . . . . . . . . 14
  
   
        |
89 | 86, 88, 4 | elab2 3216 |
. . . . . . . . . . . . 13

       |
90 | | feq2 5652 |
. . . . . . . . . . . . . 14
     
       |
91 | 90 | cbvrexv 3054 |
. . . . . . . . . . . . 13
     
       |
92 | 89, 91 | bitri 249 |
. . . . . . . . . . . 12

       |
93 | | vex 3081 |
. . . . . . . . . . . . . 14
 |
94 | | feq1 5651 |
. . . . . . . . . . . . . . 15
     
       |
95 | 94 | rexbidv 2868 |
. . . . . . . . . . . . . 14
  
   
        |
96 | 93, 95, 4 | elab2 3216 |
. . . . . . . . . . . . 13

       |
97 | | feq2 5652 |
. . . . . . . . . . . . . 14
     
       |
98 | 97 | cbvrexv 3054 |
. . . . . . . . . . . . 13
     
       |
99 | 96, 98 | bitri 249 |
. . . . . . . . . . . 12

       |
100 | 92, 99 | anbi12i 697 |
. . . . . . . . . . 11
 
               |
101 | | reeanv 2994 |
. . . . . . . . . . 11
  
                        |
102 | 100, 101 | bitr4i 252 |
. . . . . . . . . 10
 
  
            |
103 | | onss 6513 |
. . . . . . . . . . . . . . . . . . . 20
   |
104 | | ssralv 3525 |
. . . . . . . . . . . . . . . . . . . 20

 
        
           |
105 | 103, 104 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
  
        
           |
106 | 105 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
              
 
        
           |
107 | | soseq.4 |
. . . . . . . . . . . . . . . . . . . 20
 |
108 | | fveq2 5800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
109 | | fveq2 5800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
110 | 108, 109 | eqeq12d 2476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
           |
111 | 110 | rspcv 3175 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
                   |
112 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
              

 
                    |
113 | | ffvelrn 5951 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
      |
114 | | fdm 5672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
  |
115 | | eloni 4838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
116 | | ordirr 4846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

  |
117 | 115, 116 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
118 | | eleq2 2527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     |
119 | 118 | notbid 294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   |
120 | 119 | biimparc 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  
  |
121 | 117, 120 | sylan 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

  |
122 | | ndmfv 5824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
123 | | eqtr2 2481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                     |
124 | | eleq1 2526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
       |
125 | 124 | biimprd 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
             |
126 | 123, 125 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                   
   |
127 | 126 | ex 434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
                  |
128 | 121, 122,
127 | 3syl 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

                  |
129 | 128 | com23 78 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

    
             |
130 | 114, 129 | sylan2 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
             |
131 | 130 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                           |
132 | 113, 131 | syl5 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                             |
133 | 132 | exp4b 607 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     
              
      |
134 | 133 | imp32 433 |
. . . . . . . . . . . . . . . . . . . . . . 23
              

             |
135 | 112, 134 | syldd 66 |
. . . . . . . . . . . . . . . . . . . . . 22
              

 
            |
136 | 135 | com23 78 |
. . . . . . . . . . . . . . . . . . . . 21
              
 
             |
137 | 136 | imp 429 |
. . . . . . . . . . . . . . . . . . . 20
                
        

   |
138 | 107, 137 | mtoi 178 |
. . . . . . . . . . . . . . . . . . 19
                
        
  |
139 | 138 | ex 434 |
. . . . . . . . . . . . . . . . . 18
              
 
       
   |
140 | 106, 139 | syld 44 |
. . . . . . . . . . . . . . . . 17
              
 
       
   |
141 | | onss 6513 |
. . . . . . . . . . . . . . . . . . . 20
   |
142 | | ssralv 3525 |
. . . . . . . . . . . . . . . . . . . 20

 
        
           |
143 | 141, 142 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
  
        
           |
144 | 143 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
              
 
        
           |
145 | | fveq2 5800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
146 | | fveq2 5800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
147 | 145, 146 | eqeq12d 2476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
           |
148 | 147 | rspcv 3175 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
                   |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
              

 
                    |
150 | | ffvelrn 5951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
       |
151 | | fdm 5672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
  |
152 | | eloni 4838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
153 | | ordirr 4846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

  |
154 | 152, 153 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
155 | | eleq2 2527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
156 | 155 | notbid 294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   |
157 | 156 | biimparc 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  
  |
158 | | ndmfv 5824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
159 | 157, 158 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         |
160 | 154, 159 | sylan 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

      |
161 | | eqtr 2480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                     |
162 | | eleq1 2526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    
    
   |
163 | 162 | biimpd 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
        |
164 | 161, 163 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                   
   |
165 | 164 | expcom 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
                  |
166 | 165 | com23 78 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
                  |
167 | 160, 166 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

    
             |
168 | 167 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                       |
169 | 151, 168 | sylan2 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                           |
170 | 150, 169 | syl5 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                             |
171 | 170 | exp4b 607 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     
                     |
172 | 171 | com23 78 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     
                     |
173 | 172 | imp32 433 |
. . . . . . . . . . . . . . . . . . . . . . 23
              

             |
174 | 149, 173 | syldd 66 |
. . . . . . . . . . . . . . . . . . . . . 22
              

 
            |
175 | 174 | com23 78 |
. . . . . . . . . . . . . . . . . . . . 21
              
 
             |
176 | 175 | imp 429 |
. . . . . . . . . . . . . . . . . . . 20
                
        

   |
177 | 107, 176 | mtoi 178 |
. . . . . . . . . . . . . . . . . . 19
                
        
  |
178 | 177 | ex 434 |
. . . . . . . . . . . . . . . . . 18
              
 
       
   |
179 | 144, 178 | syld 44 |
. . . . . . . . . . . . . . . . 17
              
 
       
   |
180 | 140, 179 | jcad 533 |
. . . . . . . . . . . . . . . 16
              
 
        
    |
181 | | ordtri3or 4860 |
. . . . . . . . . . . . . . . . . 18
       |
182 | 115, 152,
181 | syl2an 477 |
. . . . . . . . . . . . . . . . 17
 
     |
183 | 182 | adantr 465 |
. . . . . . . . . . . . . . . 16
              

   |
184 | 180, 183 | jctird 544 |
. . . . . . . . . . . . . . 15
              
 
                 |
185 | | 3orel13 27518 |
. . . . . . . . . . . . . . . 16
     
   |
186 | 185 | imp 429 |
. . . . . . . . . . . . . . 15
      
  |
187 | 184, 186 | syl6 33 |
. . . . . . . . . . . . . 14
              
 
           |
188 | 187, 144 | jcad 533 |
. . . . . . . . . . . . 13
              
 
                      |
189 | | ffn 5668 |
. . . . . . . . . . . . . . 15
       |
190 | | ffn 5668 |
. . . . . . . . . . . . . . 15
       |
191 | | eqfnfv2 5908 |
. . . . . . . . . . . . . . 15
 
                |
192 | 189, 190,
191 | syl2an 477 |
. . . . . . . . . . . . . 14
             
            |
193 | 192 | adantl 466 |
. . . . . . . . . . . . 13
              

 
            |
194 | 188, 193 | sylibrd 234 |
. . . . . . . . . . . 12
              
 
           |
195 | 194 | ex 434 |
. . . . . . . . . . 11
 
                          |
196 | 195 | rexlimivv 2952 |
. . . . . . . . . 10
  
                       |
197 | 102, 196 | sylbi 195 |
. . . . . . . . 9
 
              |
198 | 85, 197 | syl5 32 |
. . . . . . . 8
 
    
                
   |
199 | 75, 198 | sylbird 235 |
. . . . . . 7
 
    
       
                          |
200 | 64, 199 | syl5bir 218 |
. . . . . 6
 
     
                     
                       |
201 | 53, 200 | sylbid 215 |
. . . . 5
 
           |
202 | 201 | orrd 378 |
. . . 4
 
           |
203 | | 3orcomb 975 |
. . . . 5
               |
204 | | df-3or 966 |
. . . . 5
                 |
205 | 203, 204 | bitr2i 250 |
. . . 4
        
  
     |
206 | 202, 205 | sylib 196 |
. . 3
 
         |
207 | 206 | rgen2a 2900 |
. 2


  
    |
208 | | df-so 4751 |
. 2




  
      |
209 | 6, 207, 208 | mpbir2an 911 |
1
 |