Step | Hyp | Ref
| Expression |
1 | | nss 3476 |
. . . . 5

   
          |
2 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
3 | 2 | eqeq1d 2473 |
. . . . . . . . . . 11
     
       |
4 | 3 | rspcev 3136 |
. . . . . . . . . 10
       
      |
5 | 4 | ex 441 |
. . . . . . . . 9
     

       |
6 | 5 | ad2antrl 742 |
. . . . . . . 8
                     
       |
7 | | simplr 770 |
. . . . . . . . . . . 12
               
       |
8 | | simprl 772 |
. . . . . . . . . . . 12
               
  |
9 | | r1elssi 8294 |
. . . . . . . . . . . . 13
             |
10 | 9 | sseld 3417 |
. . . . . . . . . . . 12
               |
11 | 7, 8, 10 | sylc 61 |
. . . . . . . . . . 11
               
       |
12 | | tcrank 8373 |
. . . . . . . . . . 11
                    |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
                              |
14 | 13 | eleq2d 2534 |
. . . . . . . . 9
                                |
15 | | gruelss 9237 |
. . . . . . . . . . . 12
     |
16 | | grutr 9236 |
. . . . . . . . . . . . 13

  |
17 | 16 | adantr 472 |
. . . . . . . . . . . 12
     |
18 | | vex 3034 |
. . . . . . . . . . . . 13
 |
19 | | tcmin 8243 |
. . . . . . . . . . . . 13
       
   |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . 12
 
       |
21 | 15, 17, 20 | syl2anc 673 |
. . . . . . . . . . 11
         |
22 | | rankf 8283 |
. . . . . . . . . . . . 13
          |
23 | | ffun 5742 |
. . . . . . . . . . . . 13
            |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . 12
 |
25 | | fvelima 5931 |
. . . . . . . . . . . 12
 
        
            |
26 | 24, 25 | mpan 684 |
. . . . . . . . . . 11
                     |
27 | | ssrexv 3480 |
. . . . . . . . . . 11
      
        

       |
28 | 21, 26, 27 | syl2im 38 |
. . . . . . . . . 10
   
        
       |
29 | 28 | ad2ant2r 761 |
. . . . . . . . 9
                         
       |
30 | 14, 29 | sylbid 223 |
. . . . . . . 8
                             |
31 | | simprr 774 |
. . . . . . . . . 10
               
      |
32 | | ne0i 3728 |
. . . . . . . . . . . . . . 15
   |
33 | | gruina.1 |
. . . . . . . . . . . . . . . 16
   |
34 | 33 | gruina 9261 |
. . . . . . . . . . . . . . 15
     |
35 | 32, 34 | sylan2 482 |
. . . . . . . . . . . . . 14
     |
36 | | inawina 9133 |
. . . . . . . . . . . . . 14

   |
37 | | winaon 9131 |
. . . . . . . . . . . . . 14
    |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . . . . 13
     |
39 | | r1fnon 8256 |
. . . . . . . . . . . . . 14
 |
40 | | fndm 5685 |
. . . . . . . . . . . . . 14
   |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . . . . 13
 |
42 | 38, 41 | syl6eleqr 2560 |
. . . . . . . . . . . 12
     |
43 | 42 | ad2ant2r 761 |
. . . . . . . . . . 11
               
  |
44 | | rankr1ag 8291 |
. . . . . . . . . . 11
      
             |
45 | 11, 43, 44 | syl2anc 673 |
. . . . . . . . . 10
                            |
46 | 31, 45 | mtbid 307 |
. . . . . . . . 9
                      |
47 | | rankon 8284 |
. . . . . . . . . . . . 13
     |
48 | | eloni 5440 |
. . . . . . . . . . . . . 14
    
      |
49 | | eloni 5440 |
. . . . . . . . . . . . . 14
   |
50 | | ordtri3or 5462 |
. . . . . . . . . . . . . 14
     
         
       |
51 | 48, 49, 50 | syl2an 485 |
. . . . . . . . . . . . 13
     
         
       |
52 | 47, 38, 51 | sylancr 676 |
. . . . . . . . . . . 12
       
           |
53 | | 3orass 1010 |
. . . . . . . . . . . 12
         
    
         
        |
54 | 52, 53 | sylib 201 |
. . . . . . . . . . 11
       
    
        |
55 | 54 | ord 384 |
. . . . . . . . . 10
            
        |
56 | 55 | ad2ant2r 761 |
. . . . . . . . 9
                         
        |
57 | 46, 56 | mpd 15 |
. . . . . . . 8
                    
       |
58 | 6, 30, 57 | mpjaod 388 |
. . . . . . 7
                
      |
59 | 58 | ex 441 |
. . . . . 6
              

       |
60 | 59 | exlimdv 1787 |
. . . . 5
                 
       |
61 | 1, 60 | syl5bi 225 |
. . . 4
        
    
       |
62 | | simpll 768 |
. . . . . . 7
                  |
63 | | ne0i 3728 |
. . . . . . . . . 10
   |
64 | 63, 34 | sylan2 482 |
. . . . . . . . 9
     |
65 | 64 | ad2ant2r 761 |
. . . . . . . 8
                  |
66 | 65, 36, 37 | 3syl 18 |
. . . . . . 7
                  |
67 | | simprl 772 |
. . . . . . 7
                  |
68 | | fveq2 5879 |
. . . . . . . . . 10
    
              |
69 | 68 | ad2antll 743 |
. . . . . . . . 9
                              |
70 | | elina 9130 |
. . . . . . . . . . 11
      
    |
71 | 70 | simp2bi 1046 |
. . . . . . . . . 10

      |
72 | 65, 71 | syl 17 |
. . . . . . . . 9
                      |
73 | 69, 72 | eqtrd 2505 |
. . . . . . . 8
                          |
74 | | rankcf 9220 |
. . . . . . . . 9
         |
75 | | fvex 5889 |
. . . . . . . . . 10
         |
76 | | vex 3034 |
. . . . . . . . . 10
 |
77 | | domtri 8999 |
. . . . . . . . . 10
                   
           |
78 | 75, 76, 77 | mp2an 686 |
. . . . . . . . 9
        
          |
79 | 74, 78 | mpbir 214 |
. . . . . . . 8
         |
80 | 73, 79 | syl6eqbrr 4434 |
. . . . . . 7
                  |
81 | | grudomon 9260 |
. . . . . . 7
    
  |
82 | 62, 66, 67, 80, 81 | syl112anc 1296 |
. . . . . 6
                  |
83 | | elin 3608 |
. . . . . . . . 9
       |
84 | 83 | biimpri 211 |
. . . . . . . 8
 
     |
85 | 84, 33 | syl6eleqr 2560 |
. . . . . . 7
 
   |
86 | | ordirr 5448 |
. . . . . . . . 9

  |
87 | 49, 86 | syl 17 |
. . . . . . . 8

  |
88 | 87 | adantl 473 |
. . . . . . 7
 
   |
89 | 85, 88 | pm2.21dd 179 |
. . . . . 6
 

      |
90 | 82, 66, 89 | syl2anc 673 |
. . . . 5
                      |
91 | 90 | rexlimdvaa 2872 |
. . . 4
         
   
       |
92 | 61, 91 | syld 44 |
. . 3
        
           |
93 | 92 | pm2.18d 115 |
. 2
              |
94 | 33 | grur1a 9262 |
. . 3

      |
95 | 94 | adantr 472 |
. 2
              |
96 | 93, 95 | eqssd 3435 |
1
              |