Step | Hyp | Ref
| Expression |
1 | | r19.27v 2604 |
. . . . . . . 8
   
 
            

             

            

              |
2 | | r19.28v 2605 |
. . . . . . . . 9
    
            

             

           

              |
3 | 2 | ralimi 2540 |
. . . . . . . 8
 
   
            

            
 

           

              |
4 | 1, 3 | syl 14 |
. . . . . . 7
   
 
            

            
 

           

              |
5 | | simprl 529 |
. . . . . . . . . . . . . . 15
 
  
    

   |
6 | | txlm.j |
. . . . . . . . . . . . . . . . . 18
 TopOn    |
7 | | topontop 13179 |
. . . . . . . . . . . . . . . . . 18
 TopOn 
  |
8 | 6, 7 | syl 14 |
. . . . . . . . . . . . . . . . 17
   |
9 | | txlm.k |
. . . . . . . . . . . . . . . . . 18
 TopOn    |
10 | | topontop 13179 |
. . . . . . . . . . . . . . . . . 18
 TopOn 
  |
11 | 9, 10 | syl 14 |
. . . . . . . . . . . . . . . . 17
   |
12 | | eqid 2177 |
. . . . . . . . . . . . . . . . . 18
           |
13 | 12 | txval 13422 |
. . . . . . . . . . . . . . . . 17
 
              |
14 | 8, 11, 13 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
              |
15 | 14 | adantr 276 |
. . . . . . . . . . . . . . 15
 
  
    
             |
16 | 5, 15 | eleqtrd 2256 |
. . . . . . . . . . . . . 14
 
  
    
           |
17 | | simprr 531 |
. . . . . . . . . . . . . 14
 
  
    
     |
18 | | tg2 13227 |
. . . . . . . . . . . . . 14
               


      
    |
19 | 16, 17, 18 | syl2anc 411 |
. . . . . . . . . . . . 13
 
  
    
              |
20 | | vex 2740 |
. . . . . . . . . . . . . . . 16
 |
21 | | vex 2740 |
. . . . . . . . . . . . . . . 16
 |
22 | 20, 21 | xpex 4738 |
. . . . . . . . . . . . . . 15
   |
23 | 22 | rgen2w 2533 |
. . . . . . . . . . . . . 14


   |
24 | | eqid 2177 |
. . . . . . . . . . . . . . 15
           |
25 | | eleq2 2241 |
. . . . . . . . . . . . . . . 16
               |
26 | | sseq1 3178 |
. . . . . . . . . . . . . . . 16
   
     |
27 | 25, 26 | anbi12d 473 |
. . . . . . . . . . . . . . 15
        
            |
28 | 24, 27 | rexrnmpo 5984 |
. . . . . . . . . . . . . 14
 

   


      
 


            |
29 | 23, 28 | ax-mp 5 |
. . . . . . . . . . . . 13
            


           |
30 | 19, 29 | sylib 122 |
. . . . . . . . . . . 12
 
  
    


           |
31 | 30 | ex 115 |
. . . . . . . . . . 11
    
     
            |
32 | | r19.29 2614 |
. . . . . . . . . . . . 13
   
 

           

            

          
 
   
          
 
                  

    |
33 | | r19.29 2614 |
. . . . . . . . . . . . . . 15
    

           

            
          
    
          
 
                 

    |
34 | | simprl 529 |
. . . . . . . . . . . . . . . . . . . . 21
   


                 |
35 | | opelxp 4653 |
. . . . . . . . . . . . . . . . . . . . 21
  
       |
36 | 34, 35 | sylib 122 |
. . . . . . . . . . . . . . . . . . . 20
   


          
   |
37 | | pm2.27 40 |
. . . . . . . . . . . . . . . . . . . . 21
    
          

            |
38 | | pm2.27 40 |
. . . . . . . . . . . . . . . . . . . . 21
    
          

            |
39 | 37, 38 | im2anan9 598 |
. . . . . . . . . . . . . . . . . . . 20
 
    
           

           
 

         
              |
40 | 36, 39 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
   


            

           

           
 

         
              |
41 | | txlm.z |
. . . . . . . . . . . . . . . . . . . . 21
     |
42 | 41 | rexanuz2 10984 |
. . . . . . . . . . . . . . . . . . . 20
  
              
 

         
             |
43 | 41 | uztrn2 9534 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
44 | | opelxpi 4655 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                          |
45 | | txlm.h |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
              |
46 | | fveq2 5511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
47 | | fveq2 5511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
48 | 46, 47 | opeq12d 3784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                         |
49 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
             |
50 | | txlm.f |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
51 | 50 | ad4antr 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      
                 |
52 | 51, 49 | ffvelcdmd 5648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
                 |
53 | | txlm.g |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
54 | 53 | ad4antr 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      
                 |
55 | 54, 49 | ffvelcdmd 5648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
                 |
56 | | opexg 4225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                        |
57 | 52, 55, 56 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
                        |
58 | 45, 48, 49, 57 | fvmptd3 5605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
                            |
59 | 58 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
                 
                |
60 | 44, 59 | syl5ibr 156 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
                               |
61 | | simplrr 536 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
               |
62 | 61 | sseld 3154 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
                         |
63 | 60, 62 | syld 45 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
                             |
64 | 43, 63 | sylan2 286 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
          
                        |
65 | 64 | anassrs 400 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       
         
                  |
66 | 65 | ralimdva 2544 |
. . . . . . . . . . . . . . . . . . . . 21
      
            
               
            |
67 | 66 | reximdva 2579 |
. . . . . . . . . . . . . . . . . . . 20
   


           

               

            |
68 | 42, 67 | biimtrrid 153 |
. . . . . . . . . . . . . . . . . . 19
   


                        
          
             |
69 | 40, 68 | syld 45 |
. . . . . . . . . . . . . . . . . 18
   


            

           

           

             |
70 | 69 | ex 115 |
. . . . . . . . . . . . . . . . 17
                  
           

           

              |
71 | 70 | impcomd 255 |
. . . . . . . . . . . . . . . 16
         
           

              
  
    
             |
72 | 71 | rexlimdva 2594 |
. . . . . . . . . . . . . . 15
 
  
   
           

              
  
    
             |
73 | 33, 72 | syl5 32 |
. . . . . . . . . . . . . 14
 
      
           

            
          
             |
74 | 73 | rexlimdva 2594 |
. . . . . . . . . . . . 13
    
 
 
          
 
                 
    
             |
75 | 32, 74 | syl5 32 |
. . . . . . . . . . . 12
   

 
 
          
 
            
     
    
             |
76 | 75 | expcomd 1441 |
. . . . . . . . . . 11
          

      
           

           

              |
77 | 31, 76 | syld 45 |
. . . . . . . . . 10
    
     

 
 
          
 
           

             |
78 | 77 | expdimp 259 |
. . . . . . . . 9
 

 
         
           

           

              |
79 | 78 | com23 78 |
. . . . . . . 8
 

 
 

   
          
 
               

             |
80 | 79 | ralrimdva 2557 |
. . . . . . 7
      
           

           
        

             |
81 | 4, 80 | syl5 32 |
. . . . . 6
   


            

           
        

             |
82 | 81 | adantr 276 |
. . . . 5
 

    


            

           
        

             |
83 | 8 | adantr 276 |
. . . . . . . . . . . 12
 

 
  |
84 | 11 | adantr 276 |
. . . . . . . . . . . 12
 

 
  |
85 | | simprr 531 |
. . . . . . . . . . . 12
 

 
  |
86 | | toponmax 13190 |
. . . . . . . . . . . . . 14
 TopOn 
  |
87 | 9, 86 | syl 14 |
. . . . . . . . . . . . 13
   |
88 | 87 | adantr 276 |
. . . . . . . . . . . 12
 

 
  |
89 | | txopn 13432 |
. . . . . . . . . . . 12
    
        |
90 | 83, 84, 85, 88, 89 | syl22anc 1239 |
. . . . . . . . . . 11
 

        |
91 | | eleq2 2241 |
. . . . . . . . . . . . 13
               |
92 | | eleq2 2241 |
. . . . . . . . . . . . . 14
       
         |
93 | 92 | rexralbidv 2503 |
. . . . . . . . . . . . 13
    

        

               |
94 | 91, 93 | imbi12d 234 |
. . . . . . . . . . . 12
        
                 
                |
95 | 94 | rspcv 2837 |
. . . . . . . . . . 11
      
      

                 

               |
96 | 90, 95 | syl 14 |
. . . . . . . . . 10
 

           

                
                |
97 | | simprl 529 |
. . . . . . . . . . . . 13
 

 
  |
98 | | opelxpi 4655 |
. . . . . . . . . . . . 13
 
        |
99 | 97, 98 | sylan2 286 |
. . . . . . . . . . . 12
              |
100 | 99 | expcom 116 |
. . . . . . . . . . 11
 

           |
101 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
 
   |
102 | 50 | ffvelcdmda 5647 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
103 | 53 | ffvelcdmda 5647 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
104 | 102, 103,
56 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
 
              |
105 | 45, 48, 101, 104 | fvmptd3 5605 |
. . . . . . . . . . . . . . . . . 18
 
                  |
106 | 105 | eleq1d 2246 |
. . . . . . . . . . . . . . . . 17
 
       
                |
107 | | opelxp1 4657 |
. . . . . . . . . . . . . . . . 17
             
      |
108 | 106, 107 | syl6bi 163 |
. . . . . . . . . . . . . . . 16
 
               |
109 | 43, 108 | sylan2 286 |
. . . . . . . . . . . . . . 15
 

                    |
110 | 109 | anassrs 400 |
. . . . . . . . . . . . . 14
        
      
       |
111 | 110 | ralimdva 2544 |
. . . . . . . . . . . . 13
 
  
                        |
112 | 111 | reximdva 2579 |
. . . . . . . . . . . 12
               

            |
113 | 112 | adantr 276 |
. . . . . . . . . . 11
 

                

            |
114 | 100, 113 | imim12d 74 |
. . . . . . . . . 10
 

         

              
             |
115 | 96, 114 | syld 45 |
. . . . . . . . 9
 

           

            
             |
116 | 115 | anassrs 400 |
. . . . . . . 8
      
      

           

              |
117 | 116 | ralrimdva 2557 |
. . . . . . 7
 
  
      

            
 
             |
118 | 117 | adantrl 478 |
. . . . . 6
 

           

          

 
             |
119 | 8 | adantr 276 |
. . . . . . . . . . . 12
 

 
  |
120 | 11 | adantr 276 |
. . . . . . . . . . . 12
 

 
  |
121 | | toponmax 13190 |
. . . . . . . . . . . . . 14
 TopOn 
  |
122 | 6, 121 | syl 14 |
. . . . . . . . . . . . 13
   |
123 | 122 | adantr 276 |
. . . . . . . . . . . 12
 

 
  |
124 | | simprr 531 |
. . . . . . . . . . . 12
 

    |
125 | | txopn 13432 |
. . . . . . . . . . . 12
    
        |
126 | 119, 120,
123, 124, 125 | syl22anc 1239 |
. . . . . . . . . . 11
 

        |
127 | | eleq2 2241 |
. . . . . . . . . . . . 13
               |
128 | | eleq2 2241 |
. . . . . . . . . . . . . 14
       
         |
129 | 128 | rexralbidv 2503 |
. . . . . . . . . . . . 13
    

        

               |
130 | 127, 129 | imbi12d 234 |
. . . . . . . . . . . 12
        
                 
                |
131 | 130 | rspcv 2837 |
. . . . . . . . . . 11
      
      

                 

               |
132 | 126, 131 | syl 14 |
. . . . . . . . . 10
 

           

                
                |
133 | | opelxpi 4655 |
. . . . . . . . . . . . 13
 
        |
134 | 133 | ex 115 |
. . . . . . . . . . . 12
 
 
      |
135 | 134 | ad2antrl 490 |
. . . . . . . . . . 11
 

           |
136 | 105 | eleq1d 2246 |
. . . . . . . . . . . . . . . . 17
 
       
                |
137 | | opelxp2 4658 |
. . . . . . . . . . . . . . . . 17
             
      |
138 | 136, 137 | syl6bi 163 |
. . . . . . . . . . . . . . . 16
 
               |
139 | 43, 138 | sylan2 286 |
. . . . . . . . . . . . . . 15
 

                    |
140 | 139 | anassrs 400 |
. . . . . . . . . . . . . 14
        
      
       |
141 | 140 | ralimdva 2544 |
. . . . . . . . . . . . 13
 
  
                        |
142 | 141 | reximdva 2579 |
. . . . . . . . . . . 12
               

            |
143 | 142 | adantr 276 |
. . . . . . . . . . 11
 

                

            |
144 | 135, 143 | imim12d 74 |
. . . . . . . . . 10
 

         

              
             |
145 | 132, 144 | syld 45 |
. . . . . . . . 9
 

           

            
             |
146 | 145 | anassrs 400 |
. . . . . . . 8
      
      

           

              |
147 | 146 | ralrimdva 2557 |
. . . . . . 7
 
  
      

            
 
             |
148 | 147 | adantrr 479 |
. . . . . 6
 

           

          

 
             |
149 | 118, 148 | jcad 307 |
. . . . 5
 

           

            

            

               |
150 | 82, 149 | impbid 129 |
. . . 4
 

    


            

                    
              |
151 | 150 | pm5.32da 452 |
. . 3
      

 
            

               
     


               |
152 | | opelxp 4653 |
. . . 4
  
       |
153 | 152 | anbi1i 458 |
. . 3
      
        

              
     


              |
154 | 151, 153 | bitr4di 198 |
. 2
      

 
            

                         

               |
155 | | txlm.m |
. . . . 5
   |
156 | | eqidd 2178 |
. . . . 5
 
           |
157 | 6, 41, 155, 50, 156 | lmbrf 13382 |
. . . 4
        




               |
158 | | eqidd 2178 |
. . . . 5
 
           |
159 | 9, 41, 155, 53, 158 | lmbrf 13382 |
. . . 4
        




               |
160 | 157, 159 | anbi12d 473 |
. . 3
                 
 
  

            


                |
161 | | an4 586 |
. . 3
    
 
            


            
 
   

            

               |
162 | 160, 161 | bitrdi 196 |
. 2
                 
 
   

            

                |
163 | | txtopon 13429 |
. . . 4
  TopOn  TopOn  
  TopOn      |
164 | 6, 9, 163 | syl2anc 411 |
. . 3
   TopOn 
    |
165 | 50 | ffvelcdmda 5647 |
. . . . 5
 
       |
166 | 53 | ffvelcdmda 5647 |
. . . . 5
 
       |
167 | 165, 166 | opelxpd 4656 |
. . . 4
 
                |
168 | 167, 45 | fmptd 5666 |
. . 3
         |
169 | | eqidd 2178 |
. . 3
 
           |
170 | 164, 41, 155, 168, 169 | lmbrf 13382 |
. 2
       
            
     


               |
171 | 154, 162,
170 | 3bitr4d 220 |
1
                 
          
    |