Step | Hyp | Ref
| Expression |
1 | | ltrelpr 7503 |
. . . . . . . . 9
   |
2 | 1 | brel 4678 |
. . . . . . . 8

    |
3 | | ltdfpr 7504 |
. . . . . . . . 9
 
 
     
        |
4 | 3 | biimpd 144 |
. . . . . . . 8
 
  
             |
5 | 2, 4 | mpcom 36 |
. . . . . . 7

     
       |
6 | | simprrl 539 |
. . . . . . . . . 10
 
                   |
7 | 2 | simprd 114 |
. . . . . . . . . . . . 13

  |
8 | | prop 7473 |
. . . . . . . . . . . . . . . . . 18
              |
9 | | prnmaxl 7486 |
. . . . . . . . . . . . . . . . . 18
                  
       |
10 | 8, 9 | sylan 283 |
. . . . . . . . . . . . . . . . 17
 
     
       |
11 | | ltexnqi 7407 |
. . . . . . . . . . . . . . . . . 18

     |
12 | 11 | reximi 2574 |
. . . . . . . . . . . . . . . . 17
                  |
13 | 10, 12 | syl 14 |
. . . . . . . . . . . . . . . 16
 
     
          |
14 | | df-rex 2461 |
. . . . . . . . . . . . . . . 16
                
      |
15 | 13, 14 | sylib 122 |
. . . . . . . . . . . . . . 15
 
           
      |
16 | | r19.42v 2634 |
. . . . . . . . . . . . . . . 16
         
    
      |
17 | 16 | exbii 1605 |
. . . . . . . . . . . . . . 15
        
         
      |
18 | 15, 17 | sylibr 134 |
. . . . . . . . . . . . . 14
 
            
     |
19 | | eleq1 2240 |
. . . . . . . . . . . . . . . . 17
         
       |
20 | 19 | biimparc 299 |
. . . . . . . . . . . . . . . 16
                 |
21 | 20 | reximi 2574 |
. . . . . . . . . . . . . . 15
          
        |
22 | 21 | exlimiv 1598 |
. . . . . . . . . . . . . 14
        
  
         |
23 | 18, 22 | syl 14 |
. . . . . . . . . . . . 13
 
     
        |
24 | 7, 23 | sylan 283 |
. . . . . . . . . . . 12
 
     
        |
25 | 24 | adantrl 478 |
. . . . . . . . . . 11
 
                    |
26 | 25 | adantrl 478 |
. . . . . . . . . 10
 
             
        |
27 | 6, 26 | jca 306 |
. . . . . . . . 9
 
                            |
28 | 27 | expr 375 |
. . . . . . . 8
 
      
    
    
           |
29 | 28 | reximdva 2579 |
. . . . . . 7

                 
           |
30 | 5, 29 | mpd 13 |
. . . . . 6

     
          |
31 | | r19.42v 2634 |
. . . . . . 7
             
    
          |
32 | 31 | rexbii 2484 |
. . . . . 6
  
           
     
          |
33 | 30, 32 | sylibr 134 |
. . . . 5

      
         |
34 | | rexcom 2641 |
. . . . 5
  
           
      
         |
35 | 33, 34 | sylib 122 |
. . . 4

      
         |
36 | 2 | simpld 112 |
. . . . . . . . . . . 12

  |
37 | | prop 7473 |
. . . . . . . . . . . . 13
              |
38 | | elprnqu 7480 |
. . . . . . . . . . . . 13
                    |
39 | 37, 38 | sylan 283 |
. . . . . . . . . . . 12
 
       |
40 | 36, 39 | sylan 283 |
. . . . . . . . . . 11
 
       |
41 | 40 | ex 115 |
. . . . . . . . . 10

    
   |
42 | 41 | pm4.71rd 394 |
. . . . . . . . 9

     
        |
43 | 42 | anbi1d 465 |
. . . . . . . 8

            
 
               |
44 | | anass 401 |
. . . . . . . 8
              
     
          |
45 | 43, 44 | bitrdi 196 |
. . . . . . 7

            
     
           |
46 | 45 | exbidv 1825 |
. . . . . 6

       
                          |
47 | 46 | rexbidv 2478 |
. . . . 5

        
          
    
           |
48 | | df-rex 2461 |
. . . . . 6
             
                  |
49 | 48 | rexbii 2484 |
. . . . 5
  
           
                   |
50 | 47, 49 | bitr4di 198 |
. . . 4

        
                        |
51 | 35, 50 | mpbird 167 |
. . 3

                 |
52 | | ltexprlem.1 |
. . . . . 6
        
                
          |
53 | 52 | ltexprlemell 7596 |
. . . . 5
     
                 |
54 | 53 | rexbii 2484 |
. . . 4
              
          |
55 | | ssid 3175 |
. . . . 5
 |
56 | | rexss 3222 |
. . . . 5

 
                      
           |
57 | 55, 56 | ax-mp 5 |
. . . 4
        
               
          |
58 | 54, 57 | bitr4i 187 |
. . 3
             
         |
59 | 51, 58 | sylibr 134 |
. 2

       |
60 | | nfv 1528 |
. . 3

 |
61 | | nfre1 2520 |
. . 3
  
     |
62 | | prmu 7476 |
. . . . 5
            
      |
63 | | rexex 2523 |
. . . . 5
     
       |
64 | 62, 63 | syl 14 |
. . . 4
                   |
65 | 7, 8, 64 | 3syl 17 |
. . 3

       |
66 | | elprnqu 7480 |
. . . . . . 7
                    |
67 | 8, 66 | sylan 283 |
. . . . . 6
 
       |
68 | 7, 67 | sylan 283 |
. . . . 5
 
       |
69 | | prml 7475 |
. . . . . . . . 9
            
      |
70 | 37, 69 | syl 14 |
. . . . . . . 8
        |
71 | | rexex 2523 |
. . . . . . . 8
     
       |
72 | 36, 70, 71 | 3syl 17 |
. . . . . . 7

       |
73 | 72 | adantr 276 |
. . . . . 6
 
     
      |
74 | 68 | 3adant3 1017 |
. . . . . . . . 9
 
           |
75 | | simp3 999 |
. . . . . . . . . 10
 
               |
76 | | elprnql 7479 |
. . . . . . . . . . . . . . 15
                    |
77 | 37, 76 | sylan 283 |
. . . . . . . . . . . . . 14
 
       |
78 | 36, 77 | sylan 283 |
. . . . . . . . . . . . 13
 
       |
79 | 78 | 3adant2 1016 |
. . . . . . . . . . . 12
 
           |
80 | | addcomnqg 7379 |
. . . . . . . . . . . 12
 
       |
81 | 74, 79, 80 | syl2anc 411 |
. . . . . . . . . . 11
 
               |
82 | | ltaddnq 7405 |
. . . . . . . . . . . . 13
 

    |
83 | 74, 79, 82 | syl2anc 411 |
. . . . . . . . . . . 12
 
             |
84 | | prcunqu 7483 |
. . . . . . . . . . . . . . 15
                              |
85 | 8, 84 | sylan 283 |
. . . . . . . . . . . . . 14
 
                 |
86 | 7, 85 | sylan 283 |
. . . . . . . . . . . . 13
 
                 |
87 | 86 | 3adant3 1017 |
. . . . . . . . . . . 12
 
                     |
88 | 83, 87 | mpd 13 |
. . . . . . . . . . 11
 
                 |
89 | 81, 88 | eqeltrrd 2255 |
. . . . . . . . . 10
 
                 |
90 | | 19.8a 1590 |
. . . . . . . . . 10
                             |
91 | 75, 89, 90 | syl2anc 411 |
. . . . . . . . 9
 
                         |
92 | 74, 91 | jca 306 |
. . . . . . . 8
 
                
          |
93 | 52 | ltexprlemelu 7597 |
. . . . . . . 8
     
                 |
94 | 92, 93 | sylibr 134 |
. . . . . . 7
 
               |
95 | 94 | 3expa 1203 |
. . . . . 6
  
    
           |
96 | 73, 95 | exlimddv 1898 |
. . . . 5
 
           |
97 | | 19.8a 1590 |
. . . . 5
 
       
       |
98 | 68, 96, 97 | syl2anc 411 |
. . . 4
 
       
       |
99 | | df-rex 2461 |
. . . 4
                |
100 | 98, 99 | sylibr 134 |
. . 3
 
     
      |
101 | 60, 61, 65, 100 | exlimdd 1872 |
. 2

       |
102 | 59, 101 | jca 306 |
1

     
        |