Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . . . . . . . 12
 
   |
2 | 1 | kqid 20820 |
. . . . . . . . . . 11
 TopOn 

KQ     |
3 | 2 | ad2antrr 740 |
. . . . . . . . . 10
   TopOn  KQ     
 KQ     |
4 | | cnima 20358 |
. . . . . . . . . 10
   KQ   KQ  
       |
5 | 3, 4 | sylan 479 |
. . . . . . . . 9
    TopOn  KQ   
  KQ  
       |
6 | | eleq2 2538 |
. . . . . . . . . . 11
      
        |
7 | | eleq2 2538 |
. . . . . . . . . . 11
      
        |
8 | 6, 7 | imbi12d 327 |
. . . . . . . . . 10
                        |
9 | 8 | rspcv 3132 |
. . . . . . . . 9
       
 
               |
10 | 5, 9 | syl 17 |
. . . . . . . 8
    TopOn  KQ   
  KQ  
 

                |
11 | 1 | kqffn 20817 |
. . . . . . . . . . . . 13
 TopOn 
  |
12 | 11 | ad2antrr 740 |
. . . . . . . . . . . 12
   TopOn  KQ     
  |
13 | 12 | adantr 472 |
. . . . . . . . . . 11
    TopOn  KQ   
  KQ  
  |
14 | | fnfun 5683 |
. . . . . . . . . . 11
   |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
    TopOn  KQ   
  KQ  
  |
16 | | simprl 772 |
. . . . . . . . . . . 12
   TopOn  KQ        |
17 | 16 | adantr 472 |
. . . . . . . . . . 11
    TopOn  KQ   
  KQ  
  |
18 | | fndm 5685 |
. . . . . . . . . . . 12
   |
19 | 13, 18 | syl 17 |
. . . . . . . . . . 11
    TopOn  KQ   
  KQ  
  |
20 | 17, 19 | eleqtrrd 2552 |
. . . . . . . . . 10
    TopOn  KQ   
  KQ  
  |
21 | | fvimacnv 6012 |
. . . . . . . . . 10
                |
22 | 15, 20, 21 | syl2anc 673 |
. . . . . . . . 9
    TopOn  KQ   
  KQ  
    
        |
23 | | simprr 774 |
. . . . . . . . . . . 12
   TopOn  KQ     
  |
24 | 23 | adantr 472 |
. . . . . . . . . . 11
    TopOn  KQ   
  KQ  
  |
25 | 24, 19 | eleqtrrd 2552 |
. . . . . . . . . 10
    TopOn  KQ   
  KQ  
  |
26 | | fvimacnv 6012 |
. . . . . . . . . 10
                |
27 | 15, 25, 26 | syl2anc 673 |
. . . . . . . . 9
    TopOn  KQ   
  KQ  
    
        |
28 | 22, 27 | imbi12d 327 |
. . . . . . . 8
    TopOn  KQ   
  KQ  
                          |
29 | 10, 28 | sylibrd 242 |
. . . . . . 7
    TopOn  KQ   
  KQ  
 

              |
30 | 29 | ralrimdva 2812 |
. . . . . 6
   TopOn  KQ        
  KQ                |
31 | | simplr 770 |
. . . . . . 7
   TopOn  KQ      KQ    |
32 | | fnfvelrn 6034 |
. . . . . . . . 9
 
       |
33 | 12, 16, 32 | syl2anc 673 |
. . . . . . . 8
   TopOn  KQ            |
34 | 1 | kqtopon 20819 |
. . . . . . . . . 10
 TopOn 
KQ  TopOn    |
35 | 34 | ad2antrr 740 |
. . . . . . . . 9
   TopOn  KQ      KQ  TopOn    |
36 | | toponuni 20019 |
. . . . . . . . 9
 KQ  TopOn 
 KQ    |
37 | 35, 36 | syl 17 |
. . . . . . . 8
   TopOn  KQ       KQ    |
38 | 33, 37 | eleqtrd 2551 |
. . . . . . 7
   TopOn  KQ           KQ    |
39 | | fnfvelrn 6034 |
. . . . . . . . 9
 
       |
40 | 12, 23, 39 | syl2anc 673 |
. . . . . . . 8
   TopOn  KQ            |
41 | 40, 37 | eleqtrd 2551 |
. . . . . . 7
   TopOn  KQ           KQ    |
42 | | eqid 2471 |
. . . . . . . 8
 KQ   KQ   |
43 | 42 | t1sep2 20462 |
. . . . . . 7
  KQ       KQ 
     KQ     KQ            
           |
44 | 31, 38, 41, 43 | syl3anc 1292 |
. . . . . 6
   TopOn  KQ        KQ            
           |
45 | 30, 44 | syld 44 |
. . . . 5
   TopOn  KQ        
            |
46 | 1 | kqfeq 20816 |
. . . . . . . 8
  TopOn 
         


    |
47 | | eleq2 2538 |
. . . . . . . . . 10
 
   |
48 | | eleq2 2538 |
. . . . . . . . . 10
 
   |
49 | 47, 48 | bibi12d 328 |
. . . . . . . . 9
         |
50 | 49 | cbvralv 3005 |
. . . . . . . 8
 




   |
51 | 46, 50 | syl6bbr 271 |
. . . . . . 7
  TopOn 
         


    |
52 | 51 | 3expb 1232 |
. . . . . 6
  TopOn  
 
        


    |
53 | 52 | adantlr 729 |
. . . . 5
   TopOn  KQ               
     |
54 | 45, 53 | sylibd 222 |
. . . 4
   TopOn  KQ        
 

    |
55 | 54 | ralrimivva 2814 |
. . 3
  TopOn  KQ    
   


    |
56 | 55 | ex 441 |
. 2
 TopOn 
 KQ   
   


     |
57 | | simpll 768 |
. . . . . . . . . . 11
   TopOn    TopOn    |
58 | 1 | kqopn 20826 |
. . . . . . . . . . 11
  TopOn       KQ    |
59 | 57, 58 | sylan 479 |
. . . . . . . . . 10
    TopOn 

      KQ    |
60 | | eleq2 2538 |
. . . . . . . . . . . 12
         
           |
61 | | eleq2 2538 |
. . . . . . . . . . . 12
         
           |
62 | 60, 61 | imbi12d 327 |
. . . . . . . . . . 11
                        
            |
63 | 62 | rspcv 3132 |
. . . . . . . . . 10
     KQ 
 
KQ       
    
        
            |
64 | 59, 63 | syl 17 |
. . . . . . . . 9
    TopOn 

   
KQ                                  |
65 | 1 | kqfvima 20822 |
. . . . . . . . . . . . 13
  TopOn 
 
           |
66 | 65 | 3expa 1231 |
. . . . . . . . . . . 12
   TopOn    
           |
67 | 66 | an32s 821 |
. . . . . . . . . . 11
   TopOn    
           |
68 | 67 | adantlr 729 |
. . . . . . . . . 10
    TopOn 

  
           |
69 | 1 | kqfvima 20822 |
. . . . . . . . . . . . 13
  TopOn 
 
           |
70 | 69 | 3expa 1231 |
. . . . . . . . . . . 12
   TopOn    
           |
71 | 70 | an32s 821 |
. . . . . . . . . . 11
   TopOn    
           |
72 | 71 | adantllr 733 |
. . . . . . . . . 10
    TopOn 

  
           |
73 | 68, 72 | imbi12d 327 |
. . . . . . . . 9
    TopOn 

             
            |
74 | 64, 73 | sylibrd 242 |
. . . . . . . 8
    TopOn 

   
KQ             
    |
75 | 74 | ralrimdva 2812 |
. . . . . . 7
   TopOn     
KQ             

    |
76 | 1 | kqfval 20815 |
. . . . . . . . . . 11
  TopOn       
   |
77 | 76 | adantr 472 |
. . . . . . . . . 10
   TopOn        
   |
78 | 1 | kqfval 20815 |
. . . . . . . . . . 11
  TopOn       
   |
79 | 78 | adantlr 729 |
. . . . . . . . . 10
   TopOn        
   |
80 | 77, 79 | eqeq12d 2486 |
. . . . . . . . 9
   TopOn            

 
    |
81 | | rabbi 2955 |
. . . . . . . . . 10
 



 
   |
82 | 50, 81 | bitri 257 |
. . . . . . . . 9
 



 
   |
83 | 80, 82 | syl6bbr 271 |
. . . . . . . 8
   TopOn            


    |
84 | 83 | biimprd 231 |
. . . . . . 7
   TopOn     
             |
85 | 75, 84 | imim12d 76 |
. . . . . 6
   TopOn       
 

   
KQ                         |
86 | 85 | ralimdva 2805 |
. . . . 5
  TopOn    
   


  
 
KQ       
    
            |
87 | 86 | ralimdva 2805 |
. . . 4
 TopOn 
 

 
 


  

 
KQ       
    
            |
88 | | eleq1 2537 |
. . . . . . . . . . 11
     
       |
89 | 88 | imbi1d 324 |
. . . . . . . . . 10
            
    |
90 | 89 | ralbidv 2829 |
. . . . . . . . 9
      
KQ    
 KQ            |
91 | | eqeq1 2475 |
. . . . . . . . 9
     
       |
92 | 90, 91 | imbi12d 327 |
. . . . . . . 8
        KQ    

 
KQ       
         |
93 | 92 | ralbidv 2829 |
. . . . . . 7
      
   KQ    

   
KQ       
         |
94 | 93 | ralrn 6040 |
. . . . . 6
  
     KQ    


   
KQ       
         |
95 | | eleq1 2537 |
. . . . . . . . . . 11
     
       |
96 | 95 | imbi2d 323 |
. . . . . . . . . 10
                
        |
97 | 96 | ralbidv 2829 |
. . . . . . . . 9
      
KQ        
 KQ                |
98 | | eqeq2 2482 |
. . . . . . . . 9
         
           |
99 | 97, 98 | imbi12d 327 |
. . . . . . . 8
        KQ        
       KQ            
            |
100 | 99 | ralrn 6040 |
. . . . . . 7
  
   KQ        
        KQ                         |
101 | 100 | ralbidv 2829 |
. . . . . 6
  

   KQ        
      
  KQ                         |
102 | 94, 101 | bitrd 261 |
. . . . 5
  
     KQ    



 
KQ       
    
            |
103 | 11, 102 | syl 17 |
. . . 4
 TopOn 
 
 
   KQ       
  KQ                         |
104 | 87, 103 | sylibrd 242 |
. . 3
 TopOn 
 

 
 


       
KQ   
     |
105 | | ist1-2 20440 |
. . . 4
 KQ  TopOn   KQ  
 
   KQ         |
106 | 34, 105 | syl 17 |
. . 3
 TopOn 
 KQ  
 
   KQ         |
107 | 104, 106 | sylibrd 242 |
. 2
 TopOn 
 

 
 


  KQ     |
108 | 56, 107 | impbid 195 |
1
 TopOn 
 KQ  

 
 


     |