Step | Hyp | Ref
| Expression |
1 | | tgqioo.1 |
. 2
           |
2 | | imassrn 5178 |
. . 3
       |
3 | | ioof 11729 |
. . . . . 6
  
     |
4 | | ffn 5726 |
. . . . . 6
        
   |
5 | 3, 4 | ax-mp 5 |
. . . . 5
   |
6 | | simpll 759 |
. . . . . . . . . 10
   
    
  |
7 | | elioo1 11673 |
. . . . . . . . . . . 12
       

    |
8 | 7 | biimpa 487 |
. . . . . . . . . . 11
   
    

   |
9 | 8 | simp1d 1019 |
. . . . . . . . . 10
   
    
  |
10 | 8 | simp2d 1020 |
. . . . . . . . . 10
   
    
  |
11 | | qbtwnxr 11490 |
. . . . . . . . . 10
    
   |
12 | 6, 9, 10, 11 | syl3anc 1267 |
. . . . . . . . 9
   
    
 
   |
13 | | simplr 761 |
. . . . . . . . . 10
   
    
  |
14 | 8 | simp3d 1021 |
. . . . . . . . . 10
   
    
  |
15 | | qbtwnxr 11490 |
. . . . . . . . . 10
    
   |
16 | 9, 13, 14, 15 | syl3anc 1267 |
. . . . . . . . 9
   
    
 
   |
17 | | reeanv 2957 |
. . . . . . . . . 10
  
 
 
 
 

  
    |
18 | | df-ov 6291 |
. . . . . . . . . . . . . 14
            |
19 | | opelxpi 4865 |
. . . . . . . . . . . . . . . 16
 
        |
20 | 19 | 3ad2ant2 1029 |
. . . . . . . . . . . . . . 15
   
      
  
            |
21 | | ffun 5729 |
. . . . . . . . . . . . . . . . 17
          |
22 | 3, 21 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
 |
23 | | qssre 11271 |
. . . . . . . . . . . . . . . . . . 19
 |
24 | | ressxr 9681 |
. . . . . . . . . . . . . . . . . . 19
 |
25 | 23, 24 | sstri 3440 |
. . . . . . . . . . . . . . . . . 18
 |
26 | | xpss12 4939 |
. . . . . . . . . . . . . . . . . 18
 
       |
27 | 25, 25, 26 | mp2an 677 |
. . . . . . . . . . . . . . . . 17
     |
28 | 3 | fdmi 5732 |
. . . . . . . . . . . . . . . . 17
   |
29 | 27, 28 | sseqtr4i 3464 |
. . . . . . . . . . . . . . . 16
   |
30 | | funfvima2 6139 |
. . . . . . . . . . . . . . . 16
 
                         |
31 | 22, 29, 30 | mp2an 677 |
. . . . . . . . . . . . . . 15
                     |
32 | 20, 31 | syl 17 |
. . . . . . . . . . . . . 14
   
      
  
                    |
33 | 18, 32 | syl5eqel 2532 |
. . . . . . . . . . . . 13
   
      
  
                 |
34 | 9 | 3ad2ant1 1028 |
. . . . . . . . . . . . . 14
   
      
  
       |
35 | | simp3lr 1079 |
. . . . . . . . . . . . . 14
   
      
  
       |
36 | | simp3rl 1080 |
. . . . . . . . . . . . . 14
   
      
  
       |
37 | | simp2l 1033 |
. . . . . . . . . . . . . . . 16
   
      
  
       |
38 | 25, 37 | sseldi 3429 |
. . . . . . . . . . . . . . 15
   
      
  
       |
39 | | simp2r 1034 |
. . . . . . . . . . . . . . . 16
   
      
  
       |
40 | 25, 39 | sseldi 3429 |
. . . . . . . . . . . . . . 15
   
      
  
       |
41 | | elioo1 11673 |
. . . . . . . . . . . . . . 15
       

    |
42 | 38, 40, 41 | syl2anc 666 |
. . . . . . . . . . . . . 14
   
      
  
          
    |
43 | 34, 35, 36, 42 | mpbir3and 1190 |
. . . . . . . . . . . . 13
   
      
  
           |
44 | 6 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . 15
   
      
  
       |
45 | | simp3ll 1078 |
. . . . . . . . . . . . . . . 16
   
      
  
       |
46 | | xrltle 11445 |
. . . . . . . . . . . . . . . . 17
   
   |
47 | 44, 38, 46 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
   
      
  
     
   |
48 | 45, 47 | mpd 15 |
. . . . . . . . . . . . . . 15
   
      
  
       |
49 | | iooss1 11668 |
. . . . . . . . . . . . . . 15
             |
50 | 44, 48, 49 | syl2anc 666 |
. . . . . . . . . . . . . 14
   
      
  
               |
51 | 13 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . 15
   
      
  
       |
52 | | simp3rr 1081 |
. . . . . . . . . . . . . . . 16
   
      
  
       |
53 | | xrltle 11445 |
. . . . . . . . . . . . . . . . 17
   
   |
54 | 40, 51, 53 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
   
      
  
     
   |
55 | 52, 54 | mpd 15 |
. . . . . . . . . . . . . . 15
   
      
  
       |
56 | | iooss2 11669 |
. . . . . . . . . . . . . . 15
             |
57 | 51, 55, 56 | syl2anc 666 |
. . . . . . . . . . . . . 14
   
      
  
               |
58 | 50, 57 | sstrd 3441 |
. . . . . . . . . . . . 13
   
      
  
               |
59 | | eleq2 2517 |
. . . . . . . . . . . . . . 15
     
       |
60 | | sseq1 3452 |
. . . . . . . . . . . . . . 15
     
   
           |
61 | 59, 60 | anbi12d 716 |
. . . . . . . . . . . . . 14
      
                      |
62 | 61 | rspcev 3149 |
. . . . . . . . . . . . 13
                    
              
       |
63 | 33, 43, 58, 62 | syl12anc 1265 |
. . . . . . . . . . . 12
   
      
  
             
       |
64 | 63 | 3exp 1206 |
. . . . . . . . . . 11
   
    
 
     
          
         |
65 | 64 | rexlimdvv 2884 |
. . . . . . . . . 10
   
    
 
    
          
        |
66 | 17, 65 | syl5bir 222 |
. . . . . . . . 9
   
    
  

  
          
        |
67 | 12, 16, 66 | mp2and 684 |
. . . . . . . 8
   
    
        
       |
68 | 67 | ralrimiva 2801 |
. . . . . . 7
                 
       |
69 | | qtopbas 21773 |
. . . . . . . 8
       |
70 | | eltg2b 19967 |
. . . . . . . 8
                     
              
        |
71 | 69, 70 | ax-mp 5 |
. . . . . . 7
              
              
       |
72 | 68, 71 | sylibr 216 |
. . . . . 6
                   |
73 | 72 | rgen2a 2814 |
. . . . 5
                 |
74 | | ffnov 6397 |
. . . . 5
                
 
                    |
75 | 5, 73, 74 | mpbir2an 930 |
. . . 4
  
              |
76 | | frn 5733 |
. . . 4
                
            |
77 | 75, 76 | ax-mp 5 |
. . 3
           |
78 | | 2basgen 19999 |
. . 3
       
                           |
79 | 2, 77, 78 | mp2an 677 |
. 2
               |
80 | 1, 79 | eqtr2i 2473 |
1
     |