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

   
          |
2 | | fveq2 5870 |
. . . . . . . . . . . 12
           |
3 | 2 | eqeq1d 2455 |
. . . . . . . . . . 11
     
       |
4 | 3 | rspcev 3152 |
. . . . . . . . . 10
       
      |
5 | 4 | ex 436 |
. . . . . . . . 9
     

       |
6 | 5 | ad2antrl 735 |
. . . . . . . 8
                     
       |
7 | | simplr 763 |
. . . . . . . . . . . 12
               
       |
8 | | simprl 765 |
. . . . . . . . . . . 12
               
  |
9 | | r1elssi 8281 |
. . . . . . . . . . . . 13
             |
10 | 9 | sseld 3433 |
. . . . . . . . . . . 12
               |
11 | 7, 8, 10 | sylc 62 |
. . . . . . . . . . 11
               
       |
12 | | tcrank 8360 |
. . . . . . . . . . 11
                    |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
                              |
14 | 13 | eleq2d 2516 |
. . . . . . . . 9
                                |
15 | | gruelss 9224 |
. . . . . . . . . . . 12
     |
16 | | grutr 9223 |
. . . . . . . . . . . . 13

  |
17 | 16 | adantr 467 |
. . . . . . . . . . . 12
     |
18 | | vex 3050 |
. . . . . . . . . . . . 13
 |
19 | | tcmin 8230 |
. . . . . . . . . . . . 13
       
   |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . 12
 
       |
21 | 15, 17, 20 | syl2anc 667 |
. . . . . . . . . . 11
         |
22 | | rankf 8270 |
. . . . . . . . . . . . 13
          |
23 | | ffun 5736 |
. . . . . . . . . . . . 13
            |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . 12
 |
25 | | fvelima 5922 |
. . . . . . . . . . . 12
 
        
            |
26 | 24, 25 | mpan 677 |
. . . . . . . . . . 11
                     |
27 | | ssrexv 3496 |
. . . . . . . . . . 11
      
        

       |
28 | 21, 26, 27 | syl2im 39 |
. . . . . . . . . 10
   
        
       |
29 | 28 | ad2ant2r 754 |
. . . . . . . . 9
                         
       |
30 | 14, 29 | sylbid 219 |
. . . . . . . 8
                             |
31 | | simprr 767 |
. . . . . . . . . 10
               
      |
32 | | ne0i 3739 |
. . . . . . . . . . . . . . 15
   |
33 | | gruina.1 |
. . . . . . . . . . . . . . . 16
   |
34 | 33 | gruina 9248 |
. . . . . . . . . . . . . . 15
     |
35 | 32, 34 | sylan2 477 |
. . . . . . . . . . . . . 14
     |
36 | | inawina 9120 |
. . . . . . . . . . . . . 14

   |
37 | | winaon 9118 |
. . . . . . . . . . . . . 14
    |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . . . . 13
     |
39 | | r1fnon 8243 |
. . . . . . . . . . . . . 14
 |
40 | | fndm 5680 |
. . . . . . . . . . . . . 14
   |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . . . . 13
 |
42 | 38, 41 | syl6eleqr 2542 |
. . . . . . . . . . . 12
     |
43 | 42 | ad2ant2r 754 |
. . . . . . . . . . 11
               
  |
44 | | rankr1ag 8278 |
. . . . . . . . . . 11
      
             |
45 | 11, 43, 44 | syl2anc 667 |
. . . . . . . . . 10
                            |
46 | 31, 45 | mtbid 302 |
. . . . . . . . 9
                      |
47 | | rankon 8271 |
. . . . . . . . . . . . 13
     |
48 | | eloni 5436 |
. . . . . . . . . . . . . 14
    
      |
49 | | eloni 5436 |
. . . . . . . . . . . . . 14
   |
50 | | ordtri3or 5458 |
. . . . . . . . . . . . . 14
     
         
       |
51 | 48, 49, 50 | syl2an 480 |
. . . . . . . . . . . . 13
     
         
       |
52 | 47, 38, 51 | sylancr 670 |
. . . . . . . . . . . 12
       
           |
53 | | 3orass 989 |
. . . . . . . . . . . 12
         
    
         
        |
54 | 52, 53 | sylib 200 |
. . . . . . . . . . 11
       
    
        |
55 | 54 | ord 379 |
. . . . . . . . . 10
            
        |
56 | 55 | ad2ant2r 754 |
. . . . . . . . 9
                         
        |
57 | 46, 56 | mpd 15 |
. . . . . . . 8
                    
       |
58 | 6, 30, 57 | mpjaod 383 |
. . . . . . 7
                
      |
59 | 58 | ex 436 |
. . . . . 6
              

       |
60 | 59 | exlimdv 1781 |
. . . . 5
                 
       |
61 | 1, 60 | syl5bi 221 |
. . . 4
        
    
       |
62 | | simpll 761 |
. . . . . . 7
                  |
63 | | ne0i 3739 |
. . . . . . . . . 10
   |
64 | 63, 34 | sylan2 477 |
. . . . . . . . 9
     |
65 | 64 | ad2ant2r 754 |
. . . . . . . 8
                  |
66 | 65, 36, 37 | 3syl 18 |
. . . . . . 7
                  |
67 | | simprl 765 |
. . . . . . 7
                  |
68 | | fveq2 5870 |
. . . . . . . . . 10
    
              |
69 | 68 | ad2antll 736 |
. . . . . . . . 9
                              |
70 | | elina 9117 |
. . . . . . . . . . 11
      
    |
71 | 70 | simp2bi 1025 |
. . . . . . . . . 10

      |
72 | 65, 71 | syl 17 |
. . . . . . . . 9
                      |
73 | 69, 72 | eqtrd 2487 |
. . . . . . . 8
                          |
74 | | rankcf 9207 |
. . . . . . . . 9
         |
75 | | fvex 5880 |
. . . . . . . . . 10
         |
76 | | vex 3050 |
. . . . . . . . . 10
 |
77 | | domtri 8986 |
. . . . . . . . . 10
                   
           |
78 | 75, 76, 77 | mp2an 679 |
. . . . . . . . 9
        
          |
79 | 74, 78 | mpbir 213 |
. . . . . . . 8
         |
80 | 73, 79 | syl6eqbrr 4444 |
. . . . . . 7
                  |
81 | | grudomon 9247 |
. . . . . . 7
    
  |
82 | 62, 66, 67, 80, 81 | syl112anc 1273 |
. . . . . 6
                  |
83 | | elin 3619 |
. . . . . . . . 9
       |
84 | 83 | biimpri 210 |
. . . . . . . 8
 
     |
85 | 84, 33 | syl6eleqr 2542 |
. . . . . . 7
 
   |
86 | | ordirr 5444 |
. . . . . . . . 9

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

  |
88 | 87 | adantl 468 |
. . . . . . 7
 
   |
89 | 85, 88 | pm2.21dd 178 |
. . . . . 6
 

      |
90 | 82, 66, 89 | syl2anc 667 |
. . . . 5
                      |
91 | 90 | rexlimdvaa 2882 |
. . . 4
         
   
       |
92 | 61, 91 | syld 45 |
. . 3
        
           |
93 | 92 | pm2.18d 115 |
. 2
              |
94 | 33 | grur1a 9249 |
. . 3

      |
95 | 94 | adantr 467 |
. 2
              |
96 | 93, 95 | eqssd 3451 |
1
              |