Step | Hyp | Ref
| Expression |
1 | | onelon 5448 |
. . . . 5
 
   |
2 | 1 | adantll 720 |
. . . 4
    
  |
3 | | eloni 5433 |
. . . . . . . . 9
   |
4 | | ordsucss 6645 |
. . . . . . . . 9


   |
5 | 3, 4 | syl 17 |
. . . . . . . 8
 
   |
6 | 5 | ad2antlr 733 |
. . . . . . 7
     
   |
7 | | sucelon 6644 |
. . . . . . . . . 10

  |
8 | | oveq2 6298 |
. . . . . . . . . . . . . 14
       |
9 | 8 | sseq2d 3460 |
. . . . . . . . . . . . 13
     
  
    |
10 | 9 | imbi2d 318 |
. . . . . . . . . . . 12
  
  
 

  
     |
11 | | oveq2 6298 |
. . . . . . . . . . . . . 14
       |
12 | 11 | sseq2d 3460 |
. . . . . . . . . . . . 13
   
 
  
    |
13 | 12 | imbi2d 318 |
. . . . . . . . . . . 12
    
  

  
     |
14 | | oveq2 6298 |
. . . . . . . . . . . . . 14
       |
15 | 14 | sseq2d 3460 |
. . . . . . . . . . . . 13
     
  
    |
16 | 15 | imbi2d 318 |
. . . . . . . . . . . 12
  
  
 

  
     |
17 | | oveq2 6298 |
. . . . . . . . . . . . . 14
       |
18 | 17 | sseq2d 3460 |
. . . . . . . . . . . . 13
   
 
  
    |
19 | 18 | imbi2d 318 |
. . . . . . . . . . . 12
    
  

  
     |
20 | | ssid 3451 |
. . . . . . . . . . . . 13
     |
21 | 20 | 2a1i 12 |
. . . . . . . . . . . 12
   
     |
22 | | sssucid 5500 |
. . . . . . . . . . . . . . . . 17
     |
23 | | sstr2 3439 |
. . . . . . . . . . . . . . . . 17
  
    
   
     |
24 | 22, 23 | mpi 20 |
. . . . . . . . . . . . . . . 16
  
   
    |
25 | | oasuc 7226 |
. . . . . . . . . . . . . . . . . 18
 
   
   |
26 | 25 | ancoms 455 |
. . . . . . . . . . . . . . . . 17
 
   
   |
27 | 26 | sseq2d 3460 |
. . . . . . . . . . . . . . . 16
 
       
     |
28 | 24, 27 | syl5ibr 225 |
. . . . . . . . . . . . . . 15
 
       
     |
29 | 28 | ex 436 |
. . . . . . . . . . . . . 14
 
  
          |
30 | 29 | ad2antrr 732 |
. . . . . . . . . . . . 13
  
  
  
          |
31 | 30 | a2d 29 |
. . . . . . . . . . . 12
  
     
     
      |
32 | | sucssel 5515 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
33 | 7, 32 | sylbir 217 |
. . . . . . . . . . . . . . . . . . 19
     |
34 | | limsuc 6676 |
. . . . . . . . . . . . . . . . . . . 20


   |
35 | 34 | biimpd 211 |
. . . . . . . . . . . . . . . . . . 19


   |
36 | 33, 35 | sylan9r 664 |
. . . . . . . . . . . . . . . . . 18
   
   |
37 | 36 | imp 431 |
. . . . . . . . . . . . . . . . 17
       |
38 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . 18
       |
39 | 38 | ssiun2s 4322 |
. . . . . . . . . . . . . . . . 17
  
     |
40 | 37, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
        
   |
41 | 40 | adantr 467 |
. . . . . . . . . . . . . . 15
          
   |
42 | | vex 3048 |
. . . . . . . . . . . . . . . . . . 19
 |
43 | | oalim 7234 |
. . . . . . . . . . . . . . . . . . 19
  
    
    |
44 | 42, 43 | mpanr1 689 |
. . . . . . . . . . . . . . . . . 18
      
   |
45 | 44 | ancoms 455 |
. . . . . . . . . . . . . . . . 17
      
   |
46 | 45 | adantlr 721 |
. . . . . . . . . . . . . . . 16
       
    |
47 | 46 | adantlr 721 |
. . . . . . . . . . . . . . 15
          
   |
48 | 41, 47 | sseqtr4d 3469 |
. . . . . . . . . . . . . 14
             |
49 | 48 | ex 436 |
. . . . . . . . . . . . 13
     
 
     |
50 | 49 | a1d 26 |
. . . . . . . . . . . 12
      
   
    
  
     |
51 | 10, 13, 16, 19, 21, 31, 50 | tfindsg 6687 |
. . . . . . . . . . 11
  
  
 
     |
52 | 51 | exp31 609 |
. . . . . . . . . 10
     
       |
53 | 7, 52 | syl5bi 221 |
. . . . . . . . 9
 
   
       |
54 | 53 | com4r 89 |
. . . . . . . 8
 
   
       |
55 | 54 | imp31 434 |
. . . . . . 7
     
  
    |
56 | | oasuc 7226 |
. . . . . . . . . 10
 
       |
57 | 56 | sseq1d 3459 |
. . . . . . . . 9
 
     
  
    |
58 | | ovex 6318 |
. . . . . . . . . 10
   |
59 | | sucssel 5515 |
. . . . . . . . . 10
     
         |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . 9
  
        |
61 | 57, 60 | syl6bi 232 |
. . . . . . . 8
 
             |
62 | 61 | adantlr 721 |
. . . . . . 7
                 |
63 | 6, 55, 62 | 3syld 57 |
. . . . . 6
     
       |
64 | 63 | imp 431 |
. . . . 5
             |
65 | 64 | an32s 813 |
. . . 4
             |
66 | 2, 65 | mpdan 674 |
. . 3
    
      |
67 | 66 | ex 436 |
. 2
 
         |
68 | 67 | ancoms 455 |
1
 
         |