Step | Hyp | Ref
| Expression |
1 | | dfin5 3398 |
. . . 4
  
  |
2 | | sseqin2 3642 |
. . . . 5

    |
3 | 2 | biimpi 199 |
. . . 4
     |
4 | 1, 3 | syl5reqr 2520 |
. . 3
 
   |
5 | 4 | fveq2d 5883 |
. 2
        
    |
6 | | glbcon.b |
. . . 4
     |
7 | | eqid 2471 |
. . . 4
         |
8 | | glbcon.g |
. . . 4
     |
9 | | biid 244 |
. . . 4
   
           
                  
           
                  |
10 | | id 22 |
. . . 4
   |
11 | | ssrab2 3500 |
. . . . 5

  |
12 | 11 | a1i 11 |
. . . 4
 
   |
13 | 6, 7, 8, 9, 10, 12 | glbval 16321 |
. . 3
    
      
           
                   |
14 | | hlop 32999 |
. . . 4
   |
15 | | hlclat 32995 |
. . . . . . 7
   |
16 | 6, 8 | clatglbcl 16438 |
. . . . . . 7
  
     
    |
17 | 15, 11, 16 | sylancl 675 |
. . . . . 6
    
    |
18 | 13, 17 | eqeltrrd 2550 |
. . . . 5
     
           
                   |
19 | | fvex 5889 |
. . . . . . 7
     |
20 | 6, 19 | eqeltri 2545 |
. . . . . 6
 |
21 | 20 | riotaclbBAD 32591 |
. . . . 5
    
           
                    
           
                   |
22 | 18, 21 | sylibr 217 |
. . . 4
 
 

        
 

       
          |
23 | | glbcon.o |
. . . . 5
     |
24 | | breq1 4398 |
. . . . . . 7
  
      
           |
25 | 24 | ralbidv 2829 |
. . . . . 6
  
 

         
            |
26 | | breq2 4399 |
. . . . . . . 8
  
      
           |
27 | 26 | imbi2d 323 |
. . . . . . 7
  
  

       
         
                    |
28 | 27 | ralbidv 2829 |
. . . . . 6
  
 
 

       
          
                    |
29 | 25, 28 | anbi12d 725 |
. . . . 5
  
  

        
 

       
       
 

            
                     |
30 | 6, 23, 29 | riotaocN 32846 |
. . . 4
  
  
           
                     
           
                      

           
                      |
31 | 14, 22, 30 | syl2anc 673 |
. . 3
     
           
                      

           
                      |
32 | 14 | ad2antrr 740 |
. . . . . . . . . . 11
    
  |
33 | 6, 23 | opoccl 32831 |
. . . . . . . . . . 11
 

    |
34 | 32, 33 | sylancom 680 |
. . . . . . . . . 10
    
    |
35 | 14 | ad2antrr 740 |
. . . . . . . . . . . 12
    
  |
36 | 6, 23 | opoccl 32831 |
. . . . . . . . . . . 12
 

    |
37 | 35, 36 | sylancom 680 |
. . . . . . . . . . 11
    
    |
38 | 6, 23 | opococ 32832 |
. . . . . . . . . . . . 13
 

      |
39 | 35, 38 | sylancom 680 |
. . . . . . . . . . . 12
    

     |
40 | 39 | eqcomd 2477 |
. . . . . . . . . . 11
    
      |
41 | | fveq2 5879 |
. . . . . . . . . . . . 13
  
        |
42 | 41 | eqeq2d 2481 |
. . . . . . . . . . . 12
  

         |
43 | 42 | rspcev 3136 |
. . . . . . . . . . 11
 
 
    

    |
44 | 37, 40, 43 | syl2anc 673 |
. . . . . . . . . 10
    

    |
45 | | eleq1 2537 |
. . . . . . . . . . . 12
  

     |
46 | | breq2 4399 |
. . . . . . . . . . . 12
  
                      |
47 | 45, 46 | imbi12d 327 |
. . . . . . . . . . 11
  
          
  
              |
48 | 47 | adantl 473 |
. . . . . . . . . 10
                 
  
              |
49 | 34, 44, 48 | ralxfrd 4612 |
. . . . . . . . 9
 
   
                           |
50 | | simpr 468 |
. . . . . . . . . . . 12
    
  |
51 | | simplr 770 |
. . . . . . . . . . . 12
    
  |
52 | 6, 7, 23 | oplecon3b 32837 |
. . . . . . . . . . . 12
 
                     |
53 | 32, 50, 51, 52 | syl3anc 1292 |
. . . . . . . . . . 11
    
      
             |
54 | 53 | imbi2d 323 |
. . . . . . . . . 10
    
   
      
  
              |
55 | 54 | ralbidva 2828 |
. . . . . . . . 9
 
             
                 |
56 | 49, 55 | bitr4d 264 |
. . . . . . . 8
 
   
                       |
57 | | eleq1 2537 |
. . . . . . . . 9
 
   |
58 | 57 | ralrab 3188 |
. . . . . . . 8
 

         

           |
59 | | fveq2 5879 |
. . . . . . . . . 10
  
    |
60 | 59 | eleq1d 2533 |
. . . . . . . . 9
   
     |
61 | 60 | ralrab 3188 |
. . . . . . . 8
 

                       |
62 | 56, 58, 61 | 3bitr4g 296 |
. . . . . . 7
 
   

       
 
             |
63 | 14 | ad2antrr 740 |
. . . . . . . . . 10
    
  |
64 | 6, 23 | opoccl 32831 |
. . . . . . . . . 10
 

    |
65 | 63, 64 | sylancom 680 |
. . . . . . . . 9
    
    |
66 | 14 | ad2antrr 740 |
. . . . . . . . . . 11
    
  |
67 | 6, 23 | opoccl 32831 |
. . . . . . . . . . 11
 

    |
68 | 66, 67 | sylancom 680 |
. . . . . . . . . 10
    
    |
69 | 6, 23 | opococ 32832 |
. . . . . . . . . . . 12
 

      |
70 | 66, 69 | sylancom 680 |
. . . . . . . . . . 11
    

     |
71 | 70 | eqcomd 2477 |
. . . . . . . . . 10
    
      |
72 | | fveq2 5879 |
. . . . . . . . . . . 12
  
        |
73 | 72 | eqeq2d 2481 |
. . . . . . . . . . 11
  

 
       |
74 | 73 | rspcev 3136 |
. . . . . . . . . 10
 
 
    

    |
75 | 68, 71, 74 | syl2anc 673 |
. . . . . . . . 9
    

    |
76 | | breq1 4398 |
. . . . . . . . . . . 12
  
      
           |
77 | 76 | ralbidv 2829 |
. . . . . . . . . . 11
  
 

         
            |
78 | | breq1 4398 |
. . . . . . . . . . 11
  
                      |
79 | 77, 78 | imbi12d 327 |
. . . . . . . . . 10
  
  

       
           

                      |
80 | 79 | adantl 473 |
. . . . . . . . 9
         

       
           

                      |
81 | 65, 75, 80 | ralxfrd 4612 |
. . . . . . . 8
 
     
                 
  
                
      |
82 | 14 | ad3antrrr 744 |
. . . . . . . . . . . . . . 15
         |
83 | | simpr 468 |
. . . . . . . . . . . . . . 15
         |
84 | | simplr 770 |
. . . . . . . . . . . . . . 15
         |
85 | 6, 7, 23 | oplecon3b 32837 |
. . . . . . . . . . . . . . 15
 
                     |
86 | 82, 83, 84, 85 | syl3anc 1292 |
. . . . . . . . . . . . . 14
             
             |
87 | 86 | imbi2d 323 |
. . . . . . . . . . . . 13
                                   |
88 | 87 | ralbidva 2828 |
. . . . . . . . . . . 12
    
 
  
      

  
              |
89 | 82, 33 | sylancom 680 |
. . . . . . . . . . . . 13
           |
90 | 14 | ad3antrrr 744 |
. . . . . . . . . . . . . . 15
         |
91 | 90, 36 | sylancom 680 |
. . . . . . . . . . . . . 14
           |
92 | 90, 38 | sylancom 680 |
. . . . . . . . . . . . . . 15
             |
93 | 92 | eqcomd 2477 |
. . . . . . . . . . . . . 14
      
      |
94 | 91, 93, 43 | syl2anc 673 |
. . . . . . . . . . . . 13
       
    |
95 | | breq2 4399 |
. . . . . . . . . . . . . . 15
  
                      |
96 | 45, 95 | imbi12d 327 |
. . . . . . . . . . . . . 14
  
          
  
              |
97 | 96 | adantl 473 |
. . . . . . . . . . . . 13
     
    
        
  
              |
98 | 89, 94, 97 | ralxfrd 4612 |
. . . . . . . . . . . 12
    
 
         

  
              |
99 | 88, 98 | bitr4d 264 |
. . . . . . . . . . 11
    
 
  
      


            |
100 | 60 | ralrab 3188 |
. . . . . . . . . . 11
 

                       |
101 | 57 | ralrab 3188 |
. . . . . . . . . . 11
 

         

           |
102 | 99, 100, 101 | 3bitr4g 296 |
. . . . . . . . . 10
    
 

           
            |
103 | | simplr 770 |
. . . . . . . . . . 11
    
  |
104 | | simpr 468 |
. . . . . . . . . . 11
    
  |
105 | 6, 7, 23 | oplecon3b 32837 |
. . . . . . . . . . 11
 
                     |
106 | 63, 103, 104, 105 | syl3anc 1292 |
. . . . . . . . . 10
    
      
             |
107 | 102, 106 | imbi12d 327 |
. . . . . . . . 9
    
  

         
         

                      |
108 | 107 | ralbidva 2828 |
. . . . . . . 8
 
     
                 
  
                
      |
109 | 81, 108 | bitr4d 264 |
. . . . . . 7
 
     
                 
            
          |
110 | 62, 109 | anbi12d 725 |
. . . . . 6
 
    

           
                    
                       
           |
111 | 110 | riotabidva 6286 |
. . . . 5
     
         
 

       
            
             
 

         
           |
112 | | ssrab2 3500 |
. . . . . 6

    |
113 | | glbcon.u |
. . . . . . 7
     |
114 | | biid 244 |
. . . . . . 7
              
 

         
       
 

          
 

         
          |
115 | | simpl 464 |
. . . . . . 7
      
  |
116 | | simpr 468 |
. . . . . . 7
      

     |
117 | 6, 7, 113, 114, 115, 116 | lubval 16308 |
. . . . . 6
      
   
       

          
 

         
           |
118 | 112, 117 | mpan2 685 |
. . . . 5
    
                   
 

         
           |
119 | 111, 118 | eqtr4d 2508 |
. . . 4
     
         
 

       
              
      |
120 | 119 | fveq2d 5883 |
. . 3
      

           
                        
       |
121 | 13, 31, 120 | 3eqtrd 2509 |
. 2
    
 
            |
122 | 5, 121 | sylan9eqr 2527 |
1
                   |