Step | Hyp | Ref
| Expression |
1 | | ordom 6701 |
. . . 4
 |
2 | | ordwe 5436 |
. . . 4
   |
3 | | weso 4825 |
. . . 4
  |
4 | 1, 2, 3 | mp2b 10 |
. . 3
 |
5 | 4 | a1i 11 |
. 2
 
   |
6 | | sopo 4772 |
. . . . 5
  |
7 | 4, 6 | ax-mp 5 |
. . . 4
 |
8 | | poss 4757 |
. . . 4

   |
9 | 7, 8 | mpi 20 |
. . 3

  |
10 | 9 | adantr 467 |
. 2
 
   |
11 | | fin23lem22.b |
. . . 4
    
   |
12 | 11 | fin23lem22 8757 |
. . 3
 
       |
13 | | f1ofo 5821 |
. . 3
    
      |
14 | 12, 13 | syl 17 |
. 2
 
       |
15 | | nnsdomel 8424 |
. . . . . . . 8
 
     |
16 | 15 | adantl 468 |
. . . . . . 7
  
 
  
   |
17 | 16 | biimpd 211 |
. . . . . 6
  
 
      |
18 | | fin23lem23 8756 |
. . . . . . . . . . . . 13
  
       |
19 | 18 | adantrr 723 |
. . . . . . . . . . . 12
  
 
  

   |
20 | | ineq1 3627 |
. . . . . . . . . . . . . 14
 
     |
21 | 20 | breq1d 4412 |
. . . . . . . . . . . . 13
   
     |
22 | 21 | cbvreuv 3021 |
. . . . . . . . . . . 12
   

    |
23 | 19, 22 | sylib 200 |
. . . . . . . . . . 11
  
 
  

   |
24 | | nfv 1761 |
. . . . . . . . . . . 12
       
  |
25 | 21 | cbvriotav 6263 |
. . . . . . . . . . . 12
      
 
  |
26 | | ineq1 3627 |
. . . . . . . . . . . . 13
     
      
    |
27 | 26 | breq1d 4412 |
. . . . . . . . . . . 12
     
 

      
   |
28 | 24, 25, 27 | riotaprop 6275 |
. . . . . . . . . . 11
        

    
     |
29 | 23, 28 | syl 17 |
. . . . . . . . . 10
  
 
      

    
     |
30 | 29 | simprd 465 |
. . . . . . . . 9
  
 
      
    |
31 | 30 | adantrr 723 |
. . . . . . . 8
  
           
   |
32 | | simprr 766 |
. . . . . . . . 9
  
        |
33 | | fin23lem23 8756 |
. . . . . . . . . . . . . . 15
  
       |
34 | 33 | adantrl 722 |
. . . . . . . . . . . . . 14
  
 
  

   |
35 | 20 | breq1d 4412 |
. . . . . . . . . . . . . . 15
   
     |
36 | 35 | cbvreuv 3021 |
. . . . . . . . . . . . . 14
   

    |
37 | 34, 36 | sylib 200 |
. . . . . . . . . . . . 13
  
 
  

   |
38 | | nfv 1761 |
. . . . . . . . . . . . . 14
       
  |
39 | 35 | cbvriotav 6263 |
. . . . . . . . . . . . . 14
      
 
  |
40 | | ineq1 3627 |
. . . . . . . . . . . . . . 15
     
      
    |
41 | 40 | breq1d 4412 |
. . . . . . . . . . . . . 14
     
 

      
   |
42 | 38, 39, 41 | riotaprop 6275 |
. . . . . . . . . . . . 13
        

    
     |
43 | 37, 42 | syl 17 |
. . . . . . . . . . . 12
  
 
      

    
     |
44 | 43 | simprd 465 |
. . . . . . . . . . 11
  
 
      
    |
45 | 44 | ensymd 7620 |
. . . . . . . . . 10
  
 
       
   |
46 | 45 | adantrr 723 |
. . . . . . . . 9
  
     
         |
47 | | sdomentr 7706 |
. . . . . . . . 9
 
             
   |
48 | 32, 46, 47 | syl2anc 667 |
. . . . . . . 8
  
               |
49 | | ensdomtr 7708 |
. . . . . . . 8
       

     
 
           
    |
50 | 31, 48, 49 | syl2anc 667 |
. . . . . . 7
  
           
      
   |
51 | 50 | expr 620 |
. . . . . 6
  
 
       
      
     |
52 | | simpll 760 |
. . . . . . . . 9
  
 
    |
53 | | omsson 6696 |
. . . . . . . . 9
 |
54 | 52, 53 | syl6ss 3444 |
. . . . . . . 8
  
 
    |
55 | 29 | simpld 461 |
. . . . . . . 8
  
 
         |
56 | 54, 55 | sseldd 3433 |
. . . . . . 7
  
 
         |
57 | 43 | simpld 461 |
. . . . . . . 8
  
 
         |
58 | 54, 57 | sseldd 3433 |
. . . . . . 7
  
 
         |
59 | | onsdominel 7721 |
. . . . . . . 8
     
           
      
 
      
 
   |
60 | 59 | 3expia 1210 |
. . . . . . 7
     
          
 
      
          
    |
61 | 56, 58, 60 | syl2anc 667 |
. . . . . 6
  
 
        
      
    
    
    |
62 | 17, 51, 61 | 3syld 57 |
. . . . 5
  
 
      
    
    |
63 | | simprl 764 |
. . . . . . 7
  
 
    |
64 | | breq2 4406 |
. . . . . . . . 9
   
     |
65 | 64 | riotabidv 6254 |
. . . . . . . 8
         
   |
66 | 65, 11 | fvmptg 5946 |
. . . . . . 7
     
             |
67 | 63, 55, 66 | syl2anc 667 |
. . . . . 6
  
 
             |
68 | | simprr 766 |
. . . . . . 7
  
 
    |
69 | | breq2 4406 |
. . . . . . . . 9
   
     |
70 | 69 | riotabidv 6254 |
. . . . . . . 8
         
   |
71 | 70, 11 | fvmptg 5946 |
. . . . . . 7
     
             |
72 | 68, 57, 71 | syl2anc 667 |
. . . . . 6
  
 
             |
73 | 67, 72 | eleq12d 2523 |
. . . . 5
  
 
          
      
 
    |
74 | 62, 73 | sylibrd 238 |
. . . 4
  
 
              |
75 | | epel 4748 |
. . . 4

  |
76 | | fvex 5875 |
. . . . 5
     |
77 | 76 | epelc 4747 |
. . . 4
        
          |
78 | 74, 75, 77 | 3imtr4g 274 |
. . 3
  
 
              |
79 | 78 | ralrimivva 2809 |
. 2
 
               |
80 | | soisoi 6219 |
. 2
       
  
                |
81 | 5, 10, 14, 79, 80 | syl22anc 1269 |
1
 

     |