Step | Hyp | Ref
| Expression |
1 | | fveq2 5802 |
. . . . . . . . . 10
           |
2 | | id 22 |
. . . . . . . . . 10
   |
3 | 1, 2 | eqeq12d 2476 |
. . . . . . . . 9
     
       |
4 | 3 | rspcv 3175 |
. . . . . . . 8
  
   
       |
5 | | cardon 8228 |
. . . . . . . . 9
     |
6 | | eleq1 2526 |
. . . . . . . . 9
    
        |
7 | 5, 6 | mpbii 211 |
. . . . . . . 8
    
  |
8 | 4, 7 | syl6com 35 |
. . . . . . 7
 
   

   |
9 | 8 | ssrdv 3473 |
. . . . . 6
 
   
  |
10 | | ssonuni 6511 |
. . . . . 6
      |
11 | 9, 10 | syl5 32 |
. . . . 5
  
   
    |
12 | 11 | imp 429 |
. . . 4
           |
13 | | cardonle 8241 |
. . . 4
 
        |
14 | 12, 13 | syl 16 |
. . 3
                |
15 | | cardon 8228 |
. . . . 5
      |
16 | 15 | onirri 4936 |
. . . 4
           |
17 | | eluni 4205 |
. . . . . . . 8
      
           |
18 | | elssuni 4232 |
. . . . . . . . . . . . . . . . . 18
    |
19 | | ssdomg 7468 |
. . . . . . . . . . . . . . . . . . 19
 

     |
20 | 19 | adantl 466 |
. . . . . . . . . . . . . . . . . 18
         
    |
21 | 18, 20 | syl5 32 |
. . . . . . . . . . . . . . . . 17
        
    |
22 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
    
      |
23 | | onenon 8233 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
24 | 5, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
     |
25 | 22, 24 | syl6eqelr 2551 |
. . . . . . . . . . . . . . . . . 18
    
  |
26 | | onenon 8233 |
. . . . . . . . . . . . . . . . . 18
 
   |
27 | | carddom2 8261 |
. . . . . . . . . . . . . . . . . 18
   
              |
28 | 25, 26, 27 | syl2an 477 |
. . . . . . . . . . . . . . . . 17
                      |
29 | 21, 28 | sylibrd 234 |
. . . . . . . . . . . . . . . 16
        
            |
30 | | sseq1 3488 |
. . . . . . . . . . . . . . . . 17
    
         
        |
31 | 30 | adantr 465 |
. . . . . . . . . . . . . . . 16
                 
        |
32 | 29, 31 | sylibd 214 |
. . . . . . . . . . . . . . 15
        
        |
33 | | ssel 3461 |
. . . . . . . . . . . . . . 15
                         |
34 | 32, 33 | syl6 33 |
. . . . . . . . . . . . . 14
        
                    |
35 | 34 | ex 434 |
. . . . . . . . . . . . 13
    
 
                      |
36 | 35 | com3r 79 |
. . . . . . . . . . . 12
     
 
                     |
37 | 4, 36 | syld 44 |
. . . . . . . . . . 11
  
   
 
                     |
38 | 37 | com4r 86 |
. . . . . . . . . 10
              
               |
39 | 38 | imp 429 |
. . . . . . . . 9
       
 
   
 
              |
40 | 39 | exlimiv 1689 |
. . . . . . . 8
           
   
 
              |
41 | 17, 40 | sylbi 195 |
. . . . . . 7
              
              |
42 | 41 | com13 80 |
. . . . . 6
 
     
                     |
43 | 42 | imp 429 |
. . . . 5
                             |
44 | 12, 43 | sylancom 667 |
. . . 4
                            |
45 | 16, 44 | mtoi 178 |
. . 3
                |
46 | 15 | onordi 4934 |
. . . 4
      |
47 | | eloni 4840 |
. . . . 5
 
   |
48 | 12, 47 | syl 16 |
. . . 4
           |
49 | | ordtri4 4867 |
. . . 4
               
                 |
50 | 46, 48, 49 | sylancr 663 |
. . 3
              
                 |
51 | 14, 45, 50 | mpbir2and 913 |
. 2
                |
52 | 51 | ex 434 |
1
  
   
         |