Step | Hyp | Ref
| Expression |
1 | | imasf1obl.u |
. . . . 5
  s    |
2 | | imasf1obl.v |
. . . . 5
       |
3 | | imasf1obl.f |
. . . . 5
       |
4 | | imasf1oxms.r |
. . . . 5
    |
5 | | eqid 2451 |
. . . . 5
                 |
6 | | eqid 2451 |
. . . . 5
         |
7 | | eqid 2451 |
. . . . . . . 8
         |
8 | | eqid 2451 |
. . . . . . . 8
                                 |
9 | 7, 8 | xmsxmet 21471 |
. . . . . . 7
                             |
10 | 4, 9 | syl 17 |
. . . . . 6
                            |
11 | 2 | sqxpeqd 4860 |
. . . . . . 7
               |
12 | 11 | reseq2d 5105 |
. . . . . 6
                           |
13 | 2 | fveq2d 5869 |
. . . . . 6
                 |
14 | 10, 12, 13 | 3eltr4d 2544 |
. . . . 5
                |
15 | 1, 2, 3, 4, 5, 6, 14 | imasf1oxmet 21390 |
. . . 4
            |
16 | | f1ofo 5821 |
. . . . . . 7
    
      |
17 | 3, 16 | syl 17 |
. . . . . 6
       |
18 | 1, 2, 17, 4 | imasbas 15413 |
. . . . 5
       |
19 | 18 | fveq2d 5869 |
. . . 4
                 |
20 | 15, 19 | eleqtrd 2531 |
. . 3
                |
21 | | ssid 3451 |
. . 3
         |
22 | | xmetres2 21376 |
. . 3
                                                   |
23 | 20, 21, 22 | sylancl 668 |
. 2
                            |
24 | | eqid 2451 |
. . . 4
         |
25 | | eqid 2451 |
. . . 4
         |
26 | 1, 2, 17, 4, 24, 25 | imastopn 20735 |
. . 3
          qTop
   |
27 | 24, 7, 8 | xmstopn 21466 |
. . . . . 6
                            |
28 | 4, 27 | syl 17 |
. . . . 5
                           |
29 | 12 | fveq2d 5869 |
. . . . 5
         
                         |
30 | 28, 29 | eqtr4d 2488 |
. . . 4
                   |
31 | 30 | oveq1d 6305 |
. . 3
      qTop           
   qTop    |
32 | | blbas 21445 |
. . . . . 6
                      
     |
33 | 14, 32 | syl 17 |
. . . . 5
               |
34 | | unirnbl 21435 |
. . . . . . 7
                       
     |
35 | | f1oeq2 5806 |
. . . . . . 7
             
                         |
36 | 14, 34, 35 | 3syl 18 |
. . . . . 6
                  
       |
37 | 3, 36 | mpbird 236 |
. . . . 5
            
       |
38 | | eqid 2451 |
. . . . . 6
         
   
             |
39 | 38 | tgqtop 20727 |
. . . . 5
                                                 qTop                  qTop     |
40 | 33, 37, 39 | syl2anc 667 |
. . . 4
             
    qTop                  qTop     |
41 | | eqid 2451 |
. . . . . . 7
                         |
42 | 41 | mopnval 21453 |
. . . . . 6
                                            |
43 | 14, 42 | syl 17 |
. . . . 5
         
                     |
44 | 43 | oveq1d 6305 |
. . . 4
              qTop                   qTop    |
45 | | eqid 2451 |
. . . . . . 7
                 |
46 | 45 | mopnval 21453 |
. . . . . 6
                                |
47 | 15, 46 | syl 17 |
. . . . 5
                       |
48 | | xmetf 21344 |
. . . . . . . 8
             
                    |
49 | 20, 48 | syl 17 |
. . . . . . 7
                     |
50 | | ffn 5728 |
. . . . . . 7
                                   |
51 | | fnresdm 5685 |
. . . . . . 7
                                     |
52 | 49, 50, 51 | 3syl 18 |
. . . . . 6
                       |
53 | 52 | fveq2d 5869 |
. . . . 5
                               |
54 | 3 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
    
        |
55 | | f1of1 5813 |
. . . . . . . . . . . . . . 15
    
      |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . 14
    
        |
57 | | cnvimass 5188 |
. . . . . . . . . . . . . . 15
    
 |
58 | | f1odm 5818 |
. . . . . . . . . . . . . . . 16
    
  |
59 | 54, 58 | syl 17 |
. . . . . . . . . . . . . . 15
    
 
  |
60 | 57, 59 | syl5sseq 3480 |
. . . . . . . . . . . . . 14
    
         |
61 | 14 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
    
                 |
62 | | simprl 764 |
. . . . . . . . . . . . . . 15
    
    |
63 | | simprr 766 |
. . . . . . . . . . . . . . 15
    
    |
64 | | blssm 21433 |
. . . . . . . . . . . . . . 15
              
                
  |
65 | 61, 62, 63, 64 | syl3anc 1268 |
. . . . . . . . . . . . . 14
    
            
    
  |
66 | | f1imaeq 6166 |
. . . . . . . . . . . . . 14
                                                     
     
                        |
67 | 56, 60, 65, 66 | syl12anc 1266 |
. . . . . . . . . . . . 13
    
                               
                        |
68 | 54, 16 | syl 17 |
. . . . . . . . . . . . . . 15
    
        |
69 | | simplr 762 |
. . . . . . . . . . . . . . 15
    
    |
70 | | foimacnv 5831 |
. . . . . . . . . . . . . . 15
     
            |
71 | 68, 69, 70 | syl2anc 667 |
. . . . . . . . . . . . . 14
    
             |
72 | 1 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
    
   s    |
73 | 2 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
    
        |
74 | 4 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
    
     |
75 | 72, 73, 54, 74, 5, 6, 61, 62, 63 | imasf1obl 21503 |
. . . . . . . . . . . . . . 15
    
                               
        |
76 | 75 | eqcomd 2457 |
. . . . . . . . . . . . . 14
    
                                        |
77 | 71, 76 | eqeq12d 2466 |
. . . . . . . . . . . . 13
    
                               
                   |
78 | 67, 77 | bitr3d 259 |
. . . . . . . . . . . 12
    
                  
    
                   |
79 | 78 | 2rexbidva 2907 |
. . . . . . . . . . 11
 

 

               
      
                   |
80 | 3 | adantr 467 |
. . . . . . . . . . . 12
 

      |
81 | | f1ofn 5815 |
. . . . . . . . . . . 12
    
  |
82 | | oveq1 6297 |
. . . . . . . . . . . . . . 15
                                   |
83 | 82 | eqeq2d 2461 |
. . . . . . . . . . . . . 14
                 
                   |
84 | 83 | rexbidv 2901 |
. . . . . . . . . . . . 13
      
            
                   |
85 | 84 | rexrn 6024 |
. . . . . . . . . . . 12
  
 
             
                   |
86 | 80, 81, 85 | 3syl 18 |
. . . . . . . . . . 11
 

 
 
            

                   |
87 | | forn 5796 |
. . . . . . . . . . . . 13
       |
88 | 80, 16, 87 | 3syl 18 |
. . . . . . . . . . . 12
 

  |
89 | 88 | rexeqdv 2994 |
. . . . . . . . . . 11
 

 
 
            

               |
90 | 79, 86, 89 | 3bitr2d 285 |
. . . . . . . . . 10
 

 

               
      
               |
91 | 14 | adantr 467 |
. . . . . . . . . . 11
 

     
         |
92 | | blrn 21424 |
. . . . . . . . . . 11
                            
  

                         |
93 | 91, 92 | syl 17 |
. . . . . . . . . 10
 

                  

               
        |
94 | 15 | adantr 467 |
. . . . . . . . . . 11
 

           |
95 | | blrn 21424 |
. . . . . . . . . . 11
                  

                |
96 | 94, 95 | syl 17 |
. . . . . . . . . 10
 

         

               |
97 | 90, 93, 96 | 3bitr4d 289 |
. . . . . . . . 9
 

                             |
98 | 97 | pm5.32da 647 |
. . . . . . . 8
                
    
            |
99 | | f1ofo 5821 |
. . . . . . . . . 10
                 
                   |
100 | 37, 99 | syl 17 |
. . . . . . . . 9
            
       |
101 | 38 | elqtop2 20716 |
. . . . . . . . 9
                               
              qTop 
                      |
102 | 33, 100, 101 | syl2anc 667 |
. . . . . . . 8
               qTop                
       |
103 | | blf 21422 |
. . . . . . . . . . . 12
                           |
104 | | frn 5735 |
. . . . . . . . . . . 12
                           |
105 | 15, 103, 104 | 3syl 18 |
. . . . . . . . . . 11
            |
106 | 105 | sseld 3431 |
. . . . . . . . . 10
         
    |
107 | | elpwi 3960 |
. . . . . . . . . 10
    |
108 | 106, 107 | syl6 34 |
. . . . . . . . 9
             |
109 | 108 | pm4.71rd 641 |
. . . . . . . 8
         
             |
110 | 98, 102, 109 | 3bitr4d 289 |
. . . . . . 7
               qTop 
           |
111 | 110 | eqrdv 2449 |
. . . . . 6
              qTop            |
112 | 111 | fveq2d 5869 |
. . . . 5
             
   qTop                 |
113 | 47, 53, 112 | 3eqtr4d 2495 |
. . . 4
                                     qTop     |
114 | 40, 44, 113 | 3eqtr4d 2495 |
. . 3
              qTop                        |
115 | 26, 31, 114 | 3eqtrd 2489 |
. 2
                           |
116 | | eqid 2451 |
. . 3
         |
117 | | eqid 2451 |
. . 3
                                 |
118 | 25, 116, 117 | isxms2 21463 |
. 2
 
                                                     |
119 | 23, 115, 118 | sylanbrc 670 |
1
    |