Step | Hyp | Ref
| Expression |
1 | | limuni2 5484 |
. 2
      
         |
2 | | 0ellim 5485 |
. . . 4
                 |
3 | | n0i 3736 |
. . . 4
       
         |
4 | | unieq 4206 |
. . . . . 6
                 |
5 | | uni0 4225 |
. . . . . 6
  |
6 | 4, 5 | syl6eq 2501 |
. . . . 5
                |
7 | 6 | con3i 141 |
. . . 4
       
        |
8 | 2, 3, 7 | 3syl 18 |
. . 3
       
        |
9 | | rankon 8266 |
. . . . . . . . . 10
       |
10 | 9 | onsuci 6665 |
. . . . . . . . 9
       |
11 | 10 | onsuci 6665 |
. . . . . . . 8
       |
12 | 11 | elexi 3055 |
. . . . . . 7
       |
13 | 12 | sucid 5502 |
. . . . . 6
     
       |
14 | 11 | onsuci 6665 |
. . . . . . . 8
   
   |
15 | | ontri1 5457 |
. . . . . . . 8
 
         
       
 
     
     
         |
16 | 14, 11, 15 | mp2an 678 |
. . . . . . 7
    
 
     
     
        |
17 | 16 | con2bii 334 |
. . . . . 6
    
     
 
         
    |
18 | 13, 17 | mpbi 212 |
. . . . 5
   
 
       |
19 | | rankxplim.1 |
. . . . . . 7
 |
20 | | rankxplim.2 |
. . . . . . 7
 |
21 | 19, 20 | rankxpu 8347 |
. . . . . 6
         
   |
22 | | sstr 3440 |
. . . . . 6
 
                     
      
 
        |
23 | 21, 22 | mpan2 677 |
. . . . 5
    
 
         
 
        |
24 | 18, 23 | mto 180 |
. . . 4
   
 
       |
25 | | reeanv 2958 |
. . . . 5
  
             
 
      
         |
26 | | simprl 764 |
. . . . . . . . . . . . 13
                           
    |
27 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
                        |
28 | | rankuni 8334 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
29 | | rankuni 8334 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
30 | 29 | unieqi 4207 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
31 | 28, 30 | eqtri 2473 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
32 | | df-ne 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
    |
33 | 19, 20 | xpex 6595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
34 | 33 | rankeq0 8332 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
        |
35 | 34 | notbii 298 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
        |
36 | 32, 35 | bitr2i 254 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
    |
37 | 8, 36 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . 23
            |
38 | | unixp 5369 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
        |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
                |
40 | 39 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . 21
                        |
41 | 31, 40 | syl5reqr 2500 |
. . . . . . . . . . . . . . . . . . . 20
           
            |
42 | | eqimss 3484 |
. . . . . . . . . . . . . . . . . . . 20
                  
 
          |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
           
 
          |
44 | 43 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
                                |
45 | 27, 44 | eqsstr3d 3467 |
. . . . . . . . . . . . . . . . 17
               
          |
46 | 45 | adantrr 723 |
. . . . . . . . . . . . . . . 16
                       
          |
47 | | limuni 5483 |
. . . . . . . . . . . . . . . . 17
                         |
48 | 47 | adantr 467 |
. . . . . . . . . . . . . . . 16
                                         |
49 | 46, 48 | sseqtr4d 3469 |
. . . . . . . . . . . . . . 15
                       
         |
50 | | vex 3048 |
. . . . . . . . . . . . . . . 16
 |
51 | | rankon 8266 |
. . . . . . . . . . . . . . . . . 18
       |
52 | 51 | onordi 5527 |
. . . . . . . . . . . . . . . . 17
       |
53 | | orduni 6621 |
. . . . . . . . . . . . . . . . 17
      
         |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
        |
55 | | ordelsuc 6647 |
. . . . . . . . . . . . . . . 16
         
       
          |
56 | 50, 54, 55 | mp2an 678 |
. . . . . . . . . . . . . . 15
       
         |
57 | 49, 56 | sylibr 216 |
. . . . . . . . . . . . . 14
                                 |
58 | | limsuc 6676 |
. . . . . . . . . . . . . . 15
                          |
59 | 58 | adantr 467 |
. . . . . . . . . . . . . 14
                                          |
60 | 57, 59 | mpbid 214 |
. . . . . . . . . . . . 13
                       
         |
61 | 26, 60 | eqeltrd 2529 |
. . . . . . . . . . . 12
                           
           |
62 | | limsuc 6676 |
. . . . . . . . . . . . 13
                     
                |
63 | 62 | adantr 467 |
. . . . . . . . . . . 12
                                     
                |
64 | 61, 63 | mpbid 214 |
. . . . . . . . . . 11
                       
               |
65 | | ordsucelsuc 6649 |
. . . . . . . . . . . 12
                         
            |
66 | 54, 65 | ax-mp 5 |
. . . . . . . . . . 11
    
        
               |
67 | 64, 66 | sylib 200 |
. . . . . . . . . 10
                       
               |
68 | | onsucuni2 6661 |
. . . . . . . . . . . 12
                              |
69 | 51, 68 | mpan 676 |
. . . . . . . . . . 11
                      |
70 | 69 | ad2antll 735 |
. . . . . . . . . 10
                       
               |
71 | 67, 70 | eleqtrd 2531 |
. . . . . . . . 9
                       
              |
72 | 11, 51 | onsucssi 6668 |
. . . . . . . . 9
    
       
              |
73 | 71, 72 | sylib 200 |
. . . . . . . 8
                       
              |
74 | 73 | ex 436 |
. . . . . . 7
                      
               |
75 | 74 | a1d 26 |
. . . . . 6
                
        
                |
76 | 75 | rexlimdvv 2885 |
. . . . 5
                        
               |
77 | 25, 76 | syl5bir 222 |
. . . 4
                 
      
               |
78 | 24, 77 | mtoi 182 |
. . 3
       
 
      
         |
79 | | ianor 491 |
. . . . . 6
      
         
                  |
80 | | un00 3800 |
. . . . . . . . . . . . . 14
  
    |
81 | | olc 386 |
. . . . . . . . . . . . . . 15


   |
82 | 81 | adantl 468 |
. . . . . . . . . . . . . 14
   
   |
83 | 80, 82 | sylbir 217 |
. . . . . . . . . . . . 13
  

   |
84 | | xpeq0 5257 |
. . . . . . . . . . . . 13
  
    |
85 | 83, 84 | sylibr 216 |
. . . . . . . . . . . 12
  
    |
86 | 85 | con3i 141 |
. . . . . . . . . . 11
   
   |
87 | 35, 86 | sylbir 217 |
. . . . . . . . . 10
      

   |
88 | 19, 20 | unex 6589 |
. . . . . . . . . . . 12
   |
89 | 88 | rankeq0 8332 |
. . . . . . . . . . 11
  
   
    |
90 | 89 | notbii 298 |
. . . . . . . . . 10
  
        |
91 | 87, 90 | sylib 200 |
. . . . . . . . 9
      
        |
92 | 9 | onordi 5527 |
. . . . . . . . . . 11
       |
93 | | ordzsl 6672 |
. . . . . . . . . . 11
    
                         |
94 | 92, 93 | mpbi 212 |
. . . . . . . . . 10
           
     
    |
95 | 94 | 3ori 1328 |
. . . . . . . . 9
     
             
    |
96 | 91, 95 | sylan 474 |
. . . . . . . 8
       

          
    |
97 | 96 | ex 436 |
. . . . . . 7
      
                 |
98 | | ordzsl 6672 |
. . . . . . . . . 10
             
                |
99 | 52, 98 | mpbi 212 |
. . . . . . . . 9
                      |
100 | 99 | 3ori 1328 |
. . . . . . . 8
       

               |
101 | 100 | ex 436 |
. . . . . . 7
      
                 |
102 | 97, 101 | orim12d 849 |
. . . . . 6
      
      
                           |
103 | 79, 102 | syl5bi 221 |
. . . . 5
      
      
          
                |
104 | 103 | imp 431 |
. . . 4
       
 
      
                        |
105 | | simpl 459 |
. . . . . . . 8
     
 
      
        |
106 | 34 | necon3abii 2670 |
. . . . . . . . . 10
  
        |
107 | 19, 20 | rankxplim 8350 |
. . . . . . . . . 10
     
 
            
    |
108 | 106, 107 | sylan2br 479 |
. . . . . . . . 9
     
 
      
              |
109 | | limeq 5435 |
. . . . . . . . 9
          
 
      
         |
110 | 108, 109 | syl 17 |
. . . . . . . 8
     
 
      
          
     |
111 | 105, 110 | mpbird 236 |
. . . . . . 7
     
 
      
        |
112 | 111 | expcom 437 |
. . . . . 6
      
    
 
         |
113 | | idd 25 |
. . . . . 6
      
      
         |
114 | 112, 113 | jaod 382 |
. . . . 5
      
     
        
         |
115 | 114 | adantr 467 |
. . . 4
       
 
      
             
        
         |
116 | 104, 115 | mpd 15 |
. . 3
       
 
      
       
        |
117 | 8, 78, 116 | syl2anc 667 |
. 2
       
        |
118 | 1, 117 | impbii 191 |
1
                |