Step | Hyp | Ref
| Expression |
1 | | fveq2 5887 |
. . . . . . . . . 10
           |
2 | | id 22 |
. . . . . . . . . 10
   |
3 | 1, 2 | eqeq12d 2476 |
. . . . . . . . 9
     
       |
4 | 3 | rspcv 3157 |
. . . . . . . 8
  
   
       |
5 | | cardon 8403 |
. . . . . . . . 9
     |
6 | | eleq1 2527 |
. . . . . . . . 9
    
        |
7 | 5, 6 | mpbii 216 |
. . . . . . . 8
    
  |
8 | 4, 7 | syl6com 36 |
. . . . . . 7
 
   

   |
9 | 8 | ssrdv 3449 |
. . . . . 6
 
   
  |
10 | | ssonuni 6639 |
. . . . . 6
      |
11 | 9, 10 | syl5 33 |
. . . . 5
  
   
    |
12 | 11 | imp 435 |
. . . 4
           |
13 | | cardonle 8416 |
. . . 4
 
        |
14 | 12, 13 | syl 17 |
. . 3
                |
15 | | cardon 8403 |
. . . . 5
      |
16 | 15 | onirri 5547 |
. . . 4
           |
17 | | eluni 4214 |
. . . . . . . 8
      
           |
18 | | elssuni 4240 |
. . . . . . . . . . . . . . . . . 18
    |
19 | | ssdomg 7640 |
. . . . . . . . . . . . . . . . . . 19
 

     |
20 | 19 | adantl 472 |
. . . . . . . . . . . . . . . . . 18
         
    |
21 | 18, 20 | syl5 33 |
. . . . . . . . . . . . . . . . 17
        
    |
22 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
    
      |
23 | | onenon 8408 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
24 | 5, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
     |
25 | 22, 24 | syl6eqelr 2548 |
. . . . . . . . . . . . . . . . . 18
    
  |
26 | | onenon 8408 |
. . . . . . . . . . . . . . . . . 18
 
   |
27 | | carddom2 8436 |
. . . . . . . . . . . . . . . . . 18
   
              |
28 | 25, 26, 27 | syl2an 484 |
. . . . . . . . . . . . . . . . 17
                      |
29 | 21, 28 | sylibrd 242 |
. . . . . . . . . . . . . . . 16
        
            |
30 | | sseq1 3464 |
. . . . . . . . . . . . . . . . 17
    
         
        |
31 | 30 | adantr 471 |
. . . . . . . . . . . . . . . 16
                 
        |
32 | 29, 31 | sylibd 222 |
. . . . . . . . . . . . . . 15
        
        |
33 | | ssel 3437 |
. . . . . . . . . . . . . . 15
                         |
34 | 32, 33 | syl6 34 |
. . . . . . . . . . . . . 14
        
                    |
35 | 34 | ex 440 |
. . . . . . . . . . . . 13
    
 
                      |
36 | 35 | com3r 82 |
. . . . . . . . . . . 12
     
 
                     |
37 | 4, 36 | syld 45 |
. . . . . . . . . . 11
  
   
 
                     |
38 | 37 | com4r 89 |
. . . . . . . . . 10
              
               |
39 | 38 | imp 435 |
. . . . . . . . 9
       
 
   
 
              |
40 | 39 | exlimiv 1786 |
. . . . . . . 8
           
   
 
              |
41 | 17, 40 | sylbi 200 |
. . . . . . 7
              
              |
42 | 41 | com13 83 |
. . . . . 6
 
     
                     |
43 | 42 | imp 435 |
. . . . 5
                             |
44 | 12, 43 | sylancom 678 |
. . . 4
                            |
45 | 16, 44 | mtoi 183 |
. . 3
                |
46 | 15 | onordi 5545 |
. . . 4
      |
47 | | eloni 5451 |
. . . . 5
 
   |
48 | 12, 47 | syl 17 |
. . . 4
           |
49 | | ordtri4 5478 |
. . . 4
               
                 |
50 | 46, 48, 49 | sylancr 674 |
. . 3
              
                 |
51 | 14, 45, 50 | mpbir2and 938 |
. 2
                |
52 | 51 | ex 440 |
1
  
   
         |