Step | Hyp | Ref
| Expression |
1 | | iooretop 20470 |
. . . . 5
           |
2 | | simp1 988 |
. . . . . . . . . . 11
     |
3 | 2 | a1i 11 |
. . . . . . . . . 10
      ![(,] (,]](_ioc.gif)  
      |
4 | | ltm1 10273 |
. . . . . . . . . . . . . . . 16
 
   |
5 | 4 | adantr 465 |
. . . . . . . . . . . . . . 15
 
     |
6 | | peano2rem 9779 |
. . . . . . . . . . . . . . . . 17
 
   |
7 | 6 | adantr 465 |
. . . . . . . . . . . . . . . 16
 
     |
8 | | ltletr 9570 |
. . . . . . . . . . . . . . . . 17
   
    
      |
9 | 8 | 3expb 1189 |
. . . . . . . . . . . . . . . 16
    
 
          |
10 | 7, 9 | mpancom 669 |
. . . . . . . . . . . . . . 15
 
    

     |
11 | 5, 10 | mpand 675 |
. . . . . . . . . . . . . 14
 
       |
12 | 11 | impr 619 |
. . . . . . . . . . . . 13
  
 
    |
13 | 12 | 3adantr3 1149 |
. . . . . . . . . . . 12
  
      |
14 | 13 | ex 434 |
. . . . . . . . . . 11
  
      |
15 | 14 | ad2antrr 725 |
. . . . . . . . . 10
      ![(,] (,]](_ioc.gif)  
   
    |
16 | | simp3 990 |
. . . . . . . . . . 11
     |
17 | 16 | a1i 11 |
. . . . . . . . . 10
      ![(,] (,]](_ioc.gif)  
      |
18 | 3, 15, 17 | 3jcad 1169 |
. . . . . . . . 9
      ![(,] (,]](_ioc.gif)  
    

    |
19 | | simp2 989 |
. . . . . . . . . . 11
     |
20 | 19 | a1i 11 |
. . . . . . . . . 10
      ![(,] (,]](_ioc.gif)  
      |
21 | | rexr 9533 |
. . . . . . . . . . . . 13
   |
22 | | elioc2 11462 |
. . . . . . . . . . . . 13
   
  ![(,] (,]](_ioc.gif) 

    |
23 | 21, 22 | sylan 471 |
. . . . . . . . . . . 12
 
    ![(,] (,]](_ioc.gif)       |
24 | 23 | biimpa 484 |
. . . . . . . . . . 11
      ![(,] (,]](_ioc.gif)  

   |
25 | | ltletr 9570 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
    |
26 | | ltle 9567 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
   |
27 | 26 | 3adant2 1007 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
   |
28 | 25, 27 | syld 44 |
. . . . . . . . . . . . . . . . . . . . 21
 
  
    |
29 | 28 | 3expa 1188 |
. . . . . . . . . . . . . . . . . . . 20
           |
30 | 29 | an31s 804 |
. . . . . . . . . . . . . . . . . . 19
           |
31 | 30 | imp 429 |
. . . . . . . . . . . . . . . . . 18
      
    |
32 | 31 | ancom2s 800 |
. . . . . . . . . . . . . . . . 17
        
  |
33 | 32 | an4s 822 |
. . . . . . . . . . . . . . . 16
           |
34 | 33 | 3adantr2 1148 |
. . . . . . . . . . . . . . 15
        
  |
35 | 34 | ex 434 |
. . . . . . . . . . . . . 14
    
      |
36 | 35 | anasss 647 |
. . . . . . . . . . . . 13
  
 
      |
37 | 36 | 3adantr2 1148 |
. . . . . . . . . . . 12
  
        |
38 | 37 | adantll 713 |
. . . . . . . . . . 11
    
   

   |
39 | 24, 38 | syldan 470 |
. . . . . . . . . 10
      ![(,] (,]](_ioc.gif)  
      |
40 | 3, 20, 39 | 3jcad 1169 |
. . . . . . . . 9
      ![(,] (,]](_ioc.gif)  
        |
41 | 18, 40 | jcad 533 |
. . . . . . . 8
      ![(,] (,]](_ioc.gif)  
        
     |
42 | | simpl1 991 |
. . . . . . . . 9
      
    |
43 | | simpr2 995 |
. . . . . . . . 9
      
    |
44 | | simpl3 993 |
. . . . . . . . 9
      
    |
45 | 42, 43, 44 | 3jca 1168 |
. . . . . . . 8
      
  
   |
46 | 41, 45 | impbid1 203 |
. . . . . . 7
      ![(,] (,]](_ioc.gif)  
  
  

 
     |
47 | | simpll 753 |
. . . . . . . 8
      ![(,] (,]](_ioc.gif)  
  |
48 | 24 | simp1d 1000 |
. . . . . . . . 9
      ![(,] (,]](_ioc.gif)  
  |
49 | | rexr 9533 |
. . . . . . . . 9
   |
50 | 48, 49 | syl 16 |
. . . . . . . 8
      ![(,] (,]](_ioc.gif)  
  |
51 | | elico2 11463 |
. . . . . . . 8
 
      
    |
52 | 47, 50, 51 | syl2anc 661 |
. . . . . . 7
      ![(,] (,]](_ioc.gif)  
     
    |
53 | | elin 3640 |
. . . . . . . 8
          ![[,] [,]](_icc.gif)  
      
  ![[,] [,]](_icc.gif)     |
54 | | rexr 9533 |
. . . . . . . . . . . 12
   
   |
55 | 6, 54 | syl 16 |
. . . . . . . . . . 11
 
   |
56 | 55 | ad2antrr 725 |
. . . . . . . . . 10
      ![(,] (,]](_ioc.gif)  
    |
57 | | elioo2 11445 |
. . . . . . . . . 10
           
  
    |
58 | 56, 50, 57 | syl2anc 661 |
. . . . . . . . 9
      ![(,] (,]](_ioc.gif)  
         
    |
59 | | elicc2 11464 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif)  
    |
60 | 59 | adantr 465 |
. . . . . . . . 9
      ![(,] (,]](_ioc.gif)  
   ![[,] [,]](_icc.gif)  
    |
61 | 58, 60 | anbi12d 710 |
. . . . . . . 8
      ![(,] (,]](_ioc.gif)  
       
  ![[,] [,]](_icc.gif)  
  

 
     |
62 | 53, 61 | syl5bb 257 |
. . . . . . 7
      ![(,] (,]](_ioc.gif)  
          ![[,] [,]](_icc.gif)      
       |
63 | 46, 52, 62 | 3bitr4d 285 |
. . . . . 6
      ![(,] (,]](_ioc.gif)  
           
  ![[,] [,]](_icc.gif)      |
64 | 63 | eqrdv 2448 |
. . . . 5
      ![(,] (,]](_ioc.gif)  
          
  ![[,] [,]](_icc.gif)     |
65 | | ineq1 3646 |
. . . . . . 7
       
  ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)     |
66 | 65 | eqeq2d 2465 |
. . . . . 6
               ![[,] [,]](_icc.gif)  
          
  ![[,] [,]](_icc.gif)      |
67 | 66 | rspcev 3172 |
. . . . 5
                         ![[,] [,]](_icc.gif)   
             ![[,] [,]](_icc.gif)     |
68 | 1, 64, 67 | sylancr 663 |
. . . 4
      ![(,] (,]](_ioc.gif)  
             ![[,] [,]](_icc.gif)     |
69 | | retop 20465 |
. . . . 5
     |
70 | | ovex 6218 |
. . . . 5
  ![[,] [,]](_icc.gif)   |
71 | | elrest 14477 |
. . . . 5
        ![[,] [,]](_icc.gif)             ↾t   ![[,] [,]](_icc.gif)   
  
         ![[,] [,]](_icc.gif)      |
72 | 69, 70, 71 | mp2an 672 |
. . . 4
         
↾t   ![[,] [,]](_icc.gif)  
             ![[,] [,]](_icc.gif)     |
73 | 68, 72 | sylibr 212 |
. . 3
      ![(,] (,]](_ioc.gif)  
         ↾t   ![[,] [,]](_icc.gif)     |
74 | | iccssre 11481 |
. . . . 5
 
   ![[,] [,]](_icc.gif) 
  |
75 | 74 | adantr 465 |
. . . 4
      ![(,] (,]](_ioc.gif)  
  ![[,] [,]](_icc.gif)    |
76 | | eqid 2451 |
. . . . 5
         |
77 | | icoopnst.1 |
. . . . 5
        ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      |
78 | 76, 77 | resubmet 20504 |
. . . 4
   ![[,] [,]](_icc.gif) 
     ↾t   ![[,] [,]](_icc.gif)     |
79 | 75, 78 | syl 16 |
. . 3
      ![(,] (,]](_ioc.gif)  
     ↾t   ![[,] [,]](_icc.gif)     |
80 | 73, 79 | eleqtrrd 2542 |
. 2
      ![(,] (,]](_ioc.gif)  
      |
81 | 80 | ex 434 |
1
 
    ![(,] (,]](_ioc.gif)         |