Step | Hyp | Ref
| Expression |
1 | | f1ofo 5826 |
. . . . 5
    
      |
2 | | qtopcmp.1 |
. . . . . . 7
  |
3 | 2 | elqtop2 20728 |
. . . . . 6
         qTop 
          |
4 | 2 | elqtop2 20728 |
. . . . . 6
         qTop 
          |
5 | 3, 4 | anbi12d 718 |
. . . . 5
          qTop 
 qTop  
 
                 |
6 | 1, 5 | sylan2 477 |
. . . 4
          qTop 
 qTop  
 
                 |
7 | | simpl1l 1060 |
. . . . . . . . 9
        
                    |
8 | | simpl2r 1063 |
. . . . . . . . 9
        
                         |
9 | | simpl3r 1065 |
. . . . . . . . 9
        
                         |
10 | | simpl1r 1061 |
. . . . . . . . . . . 12
        
                        |
11 | | f1ocnv 5831 |
. . . . . . . . . . . 12
    
       |
12 | | f1ofn 5820 |
. . . . . . . . . . . 12
      
  |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . 11
        
                  
  |
14 | | simpl2l 1062 |
. . . . . . . . . . 11
        
                    |
15 | | inss1 3654 |
. . . . . . . . . . . 12
   |
16 | | simpr 463 |
. . . . . . . . . . . 12
        
                      |
17 | 15, 16 | sseldi 3432 |
. . . . . . . . . . 11
        
                    |
18 | | fnfvima 6148 |
. . . . . . . . . . 11
  
             |
19 | 13, 14, 17, 18 | syl3anc 1269 |
. . . . . . . . . 10
        
                              |
20 | | simpl3l 1064 |
. . . . . . . . . . 11
        
                    |
21 | | inss2 3655 |
. . . . . . . . . . . 12
   |
22 | 21, 16 | sseldi 3432 |
. . . . . . . . . . 11
        
                    |
23 | | fnfvima 6148 |
. . . . . . . . . . 11
  
             |
24 | 13, 20, 22, 23 | syl3anc 1269 |
. . . . . . . . . 10
        
                              |
25 | 19, 24 | elind 3620 |
. . . . . . . . 9
        
                                     |
26 | | basis2 19978 |
. . . . . . . . 9
                                  
     
               |
27 | 7, 8, 9, 25, 26 | syl22anc 1270 |
. . . . . . . 8
        
                  
                     |
28 | 10 | adantr 467 |
. . . . . . . . . . 11
    
     
                       
                     |
29 | | simp2l 1035 |
. . . . . . . . . . . . . 14
        
                |
30 | 15, 29 | syl5ss 3445 |
. . . . . . . . . . . . 13
        
              
   |
31 | 30 | sselda 3434 |
. . . . . . . . . . . 12
        
                    |
32 | 31 | adantr 467 |
. . . . . . . . . . 11
    
     
                       
                 |
33 | | f1ocnvfv2 6181 |
. . . . . . . . . . 11
     
            |
34 | 28, 32, 33 | syl2anc 667 |
. . . . . . . . . 10
    
     
                       
                          |
35 | | f1ofn 5820 |
. . . . . . . . . . . 12
    
  |
36 | 28, 35 | syl 17 |
. . . . . . . . . . 11
    
     
                       
                 |
37 | | simprrr 776 |
. . . . . . . . . . . . 13
    
     
                       
                             |
38 | | inss1 3654 |
. . . . . . . . . . . . 13
                  |
39 | 37, 38 | syl6ss 3446 |
. . . . . . . . . . . 12
    
     
                       
                      |
40 | | cnvimass 5191 |
. . . . . . . . . . . . 13
    
 |
41 | | f1odm 5823 |
. . . . . . . . . . . . . 14
    
  |
42 | 28, 41 | syl 17 |
. . . . . . . . . . . . 13
    
     
                       
                 |
43 | 40, 42 | syl5sseq 3482 |
. . . . . . . . . . . 12
    
     
                       
                      |
44 | 39, 43 | sstrd 3444 |
. . . . . . . . . . 11
    
     
                       
                 |
45 | | simprrl 775 |
. . . . . . . . . . 11
    
     
                       
                      |
46 | | fnfvima 6148 |
. . . . . . . . . . 11
                       |
47 | 36, 44, 45, 46 | syl3anc 1269 |
. . . . . . . . . 10
    
     
                       
                              |
48 | 34, 47 | eqeltrrd 2532 |
. . . . . . . . 9
    
     
                       
                     |
49 | | imassrn 5182 |
. . . . . . . . . . . 12
     |
50 | 28, 1 | syl 17 |
. . . . . . . . . . . . 13
    
     
                       
                     |
51 | | forn 5801 |
. . . . . . . . . . . . 13
       |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . 12
    
     
                       
                 |
53 | 49, 52 | syl5sseq 3482 |
. . . . . . . . . . 11
    
     
                       
                     |
54 | | f1of1 5818 |
. . . . . . . . . . . . . 14
    
      |
55 | 28, 54 | syl 17 |
. . . . . . . . . . . . 13
    
     
                       
                     |
56 | | f1imacnv 5835 |
. . . . . . . . . . . . 13
     
            |
57 | 55, 44, 56 | syl2anc 667 |
. . . . . . . . . . . 12
    
     
                       
                          |
58 | | simprl 765 |
. . . . . . . . . . . 12
    
     
                       
                 |
59 | 57, 58 | eqeltrd 2531 |
. . . . . . . . . . 11
    
     
                       
                          |
60 | 7 | adantr 467 |
. . . . . . . . . . . 12
    
     
                       
                 |
61 | 2 | elqtop2 20728 |
. . . . . . . . . . . 12
             qTop 
                  |
62 | 60, 50, 61 | syl2anc 667 |
. . . . . . . . . . 11
    
     
                       
                     qTop 
                  |
63 | 53, 59, 62 | mpbir2and 934 |
. . . . . . . . . 10
    
     
                       
                    qTop    |
64 | | fnfun 5678 |
. . . . . . . . . . . . . 14
   |
65 | | inpreima 6012 |
. . . . . . . . . . . . . 14

                     |
66 | 36, 64, 65 | 3syl 18 |
. . . . . . . . . . . . 13
    
     
                       
                                    |
67 | 37, 66 | sseqtr4d 3471 |
. . . . . . . . . . . 12
    
     
                       
                        |
68 | 36, 64 | syl 17 |
. . . . . . . . . . . . 13
    
     
                       
                 |
69 | 39, 40 | syl6ss 3446 |
. . . . . . . . . . . . 13
    
     
                       
                 |
70 | | funimass3 6003 |
. . . . . . . . . . . . 13
        
           |
71 | 68, 69, 70 | syl2anc 667 |
. . . . . . . . . . . 12
    
     
                       
                   
 
          |
72 | 67, 71 | mpbird 236 |
. . . . . . . . . . 11
    
     
                       
                   
   |
73 | | vex 3050 |
. . . . . . . . . . . . 13
 |
74 | 73 | inex1 4547 |
. . . . . . . . . . . 12
   |
75 | 74 | elpw2 4570 |
. . . . . . . . . . 11
       
    
   |
76 | 72, 75 | sylibr 216 |
. . . . . . . . . 10
    
     
                       
                        |
77 | 63, 76 | elind 3620 |
. . . . . . . . 9
    
     
                       
                     qTop 
 
    |
78 | | elunii 4206 |
. . . . . . . . 9
            qTop   
      qTop
       |
79 | 48, 77, 78 | syl2anc 667 |
. . . . . . . 8
    
     
                       
                  qTop   
    |
80 | 27, 79 | rexlimddv 2885 |
. . . . . . 7
        
                     qTop   
    |
81 | 80 | ex 436 |
. . . . . 6
        
                    qTop
        |
82 | 81 | ssrdv 3440 |
. . . . 5
        
              
    qTop   
    |
83 | 82 | 3expib 1212 |
. . . 4
               
             qTop
        |
84 | 6, 83 | sylbid 219 |
. . 3
          qTop 
 qTop   
    qTop   
     |
85 | 84 | ralrimivv 2810 |
. 2
         qTop     qTop        qTop   
    |
86 | | ovex 6323 |
. . 3
 qTop   |
87 | | isbasisg 19974 |
. . 3
  qTop    qTop 
  qTop     qTop        qTop   
     |
88 | 86, 87 | ax-mp 5 |
. 2
  qTop    qTop     qTop    
   qTop
       |
89 | 85, 88 | sylibr 216 |
1
        qTop    |