Step | Hyp | Ref
| Expression |
1 | | o1f 13641 |
. . . 4
   
      |
2 | | o1bdd 13643 |
. . . 4
            
 
           |
3 | 1, 2 | mpdan 679 |
. . 3
   
                |
4 | 3 | adantr 471 |
. 2
        
                |
5 | | o1f 13641 |
. . . 4
   
      |
6 | | o1bdd 13643 |
. . . 4
            
 
           |
7 | 5, 6 | mpdan 679 |
. . 3
   
                |
8 | 7 | adantl 472 |
. 2
        
                |
9 | | reeanv 2969 |
. . 3
  
 
          
            
                 
                |
10 | | reeanv 2969 |
. . . . 5
  
 
         
           
                
               |
11 | | inss1 3663 |
. . . . . . . . . 10


 |
12 | | ssralv 3504 |
. . . . . . . . . 10
  
                              |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
 
 
         
   
           |
14 | | inss2 3664 |
. . . . . . . . . 10


 |
15 | | ssralv 3504 |
. . . . . . . . . 10
  
                              |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . 9
 
 
         
   
           |
17 | 13, 16 | anim12i 574 |
. . . . . . . 8
            
           
 
 

          
     
            |
18 | | r19.26 2928 |
. . . . . . . 8
 

   
        

         
 

          
     
            |
19 | 17, 18 | sylibr 217 |
. . . . . . 7
            
           
 
     
                 
    |
20 | | prth 579 |
. . . . . . . . . 10
          
         
 
 
         
            |
21 | | simplrl 775 |
. . . . . . . . . . . . . 14
              
 
  |
22 | 21 | adantr 471 |
. . . . . . . . . . . . 13
               
       |
23 | | simplrr 776 |
. . . . . . . . . . . . . 14
              
 
  |
24 | 23 | adantr 471 |
. . . . . . . . . . . . 13
               
       |
25 | | o1dm 13642 |
. . . . . . . . . . . . . . . 16
   
  |
26 | 25 | ad3antrrr 741 |
. . . . . . . . . . . . . . 15
              
 
  |
27 | 11, 26 | syl5ss 3454 |
. . . . . . . . . . . . . 14
              
 

   |
28 | 27 | sselda 3443 |
. . . . . . . . . . . . 13
               
       |
29 | | maxle 11513 |
. . . . . . . . . . . . 13
 
      
     |
30 | 22, 24, 28, 29 | syl3anc 1276 |
. . . . . . . . . . . 12
               
           
    |
31 | 30 | biimpd 212 |
. . . . . . . . . . 11
               
          
     |
32 | 1 | ad3antrrr 741 |
. . . . . . . . . . . . . 14
              
 
      |
33 | 11 | sseli 3439 |
. . . . . . . . . . . . . 14
     |
34 | | ffvelrn 6042 |
. . . . . . . . . . . . . 14
      
      |
35 | 32, 33, 34 | syl2an 484 |
. . . . . . . . . . . . 13
               
           |
36 | 5 | ad3antlr 742 |
. . . . . . . . . . . . . 14
              
 
      |
37 | 14 | sseli 3439 |
. . . . . . . . . . . . . 14
     |
38 | | ffvelrn 6042 |
. . . . . . . . . . . . . 14
      
      |
39 | 36, 37, 38 | syl2an 484 |
. . . . . . . . . . . . 13
               
           |
40 | | o1of2.3 |
. . . . . . . . . . . . . . 15
                
        
   |
41 | 40 | ralrimivva 2820 |
. . . . . . . . . . . . . 14
 
        
            
   |
42 | 41 | ad2antlr 738 |
. . . . . . . . . . . . 13
               
     
      
            
   |
43 | | fveq2 5887 |
. . . . . . . . . . . . . . . . 17
                   |
44 | 43 | breq1d 4425 |
. . . . . . . . . . . . . . . 16
         
           |
45 | 44 | anbi1d 716 |
. . . . . . . . . . . . . . 15
          
    
            
    |
46 | | oveq1 6321 |
. . . . . . . . . . . . . . . . 17
                   |
47 | 46 | fveq2d 5891 |
. . . . . . . . . . . . . . . 16
                           |
48 | 47 | breq1d 4425 |
. . . . . . . . . . . . . . 15
             
               |
49 | 45, 48 | imbi12d 326 |
. . . . . . . . . . . . . 14
               
        
          
                
    |
50 | | fveq2 5887 |
. . . . . . . . . . . . . . . . 17
                   |
51 | 50 | breq1d 4425 |
. . . . . . . . . . . . . . . 16
         
           |
52 | 51 | anbi2d 715 |
. . . . . . . . . . . . . . 15
              
    
                
    |
53 | | oveq2 6322 |
. . . . . . . . . . . . . . . . 17
                           |
54 | 53 | fveq2d 5891 |
. . . . . . . . . . . . . . . 16
                                   |
55 | 54 | breq1d 4425 |
. . . . . . . . . . . . . . 15
                 
                   |
56 | 52, 55 | imbi12d 326 |
. . . . . . . . . . . . . 14
                   
            
          
                        
    |
57 | 49, 56 | rspc2va 3171 |
. . . . . . . . . . . . 13
                                                    
                
   |
58 | 35, 39, 42, 57 | syl21anc 1275 |
. . . . . . . . . . . 12
               
                      
                
   |
59 | | ffn 5750 |
. . . . . . . . . . . . . . . 16
       |
60 | 32, 59 | syl 17 |
. . . . . . . . . . . . . . 15
              
 
  |
61 | | ffn 5750 |
. . . . . . . . . . . . . . . 16
       |
62 | 36, 61 | syl 17 |
. . . . . . . . . . . . . . 15
              
 
  |
63 | | reex 9655 |
. . . . . . . . . . . . . . . 16
 |
64 | | ssexg 4562 |
. . . . . . . . . . . . . . . 16
     |
65 | 26, 63, 64 | sylancl 673 |
. . . . . . . . . . . . . . 15
              
 
  |
66 | | dmexg 6750 |
. . . . . . . . . . . . . . . 16
   
  |
67 | 66 | ad3antlr 742 |
. . . . . . . . . . . . . . 15
              
 
  |
68 | | eqid 2461 |
. . . . . . . . . . . . . . 15

    |
69 | | eqidd 2462 |
. . . . . . . . . . . . . . 15
               
             |
70 | | eqidd 2462 |
. . . . . . . . . . . . . . 15
               
             |
71 | 60, 62, 65, 67, 68, 69, 70 | ofval 6566 |
. . . . . . . . . . . . . 14
               
                            |
72 | 71 | fveq2d 5891 |
. . . . . . . . . . . . 13
               
                                    |
73 | 72 | breq1d 4425 |
. . . . . . . . . . . 12
               
                                  
   |
74 | 58, 73 | sylibrd 242 |
. . . . . . . . . . 11
               
                      
                 |
75 | 31, 74 | imim12d 77 |
. . . . . . . . . 10
               
                 
            
               
    |
76 | 20, 75 | syl5 33 |
. . . . . . . . 9
               
                 
            
               
    |
77 | 76 | ralimdva 2807 |
. . . . . . . 8
              
 
 

   
        

                   
                 |
78 | | o1of2.2 |
. . . . . . . . . . 11
 
       |
79 | 78 | adantl 472 |
. . . . . . . . . 10
               
           |
80 | 79, 32, 36, 65, 67, 68 | off 6572 |
. . . . . . . . 9
              
 
       
     |
81 | 23, 21 | ifcld 3935 |
. . . . . . . . 9
              
 
 
     |
82 | | o1of2.1 |
. . . . . . . . . 10
 
   |
83 | 82 | adantl 472 |
. . . . . . . . 9
              
 
  |
84 | | elo12r 13640 |
. . . . . . . . . 10
                
     
       
               
 
          |
85 | 84 | 3expia 1217 |
. . . . . . . . 9
                
     
 
 

       
                         |
86 | 80, 27, 81, 83, 85 | syl22anc 1277 |
. . . . . . . 8
              
 
 

       
                         |
87 | 77, 86 | syld 45 |
. . . . . . 7
              
 
 

   
        

                     |
88 | 19, 87 | syl5 33 |
. . . . . 6
              
 
  
         
           
 
           |
89 | 88 | rexlimdvva 2897 |
. . . . 5
            
 
              
 
                     |
90 | 10, 89 | syl5bir 226 |
. . . 4
            
  
          
            
 
           |
91 | 90 | rexlimdvva 2897 |
. . 3
        
 
               
                        |
92 | 9, 91 | syl5bir 226 |
. 2
        
  
 
 
          
                        |
93 | 4, 8, 92 | mp2and 690 |
1
        
          |