Step | Hyp | Ref
| Expression |
1 | | fveq2 5517 |
. . . . . . 7
                       |
2 | | df-ov 5881 |
. . . . . . 7
   
              |
3 | 1, 2 | eqtr4di 2228 |
. . . . . 6
                    |
4 | | fveq2 5517 |
. . . . . . 7
                       |
5 | | df-ov 5881 |
. . . . . . 7
   
              |
6 | 4, 5 | eqtr4di 2228 |
. . . . . 6
                    |
7 | 3, 6 | opeq12d 3788 |
. . . . 5
                                 
      |
8 | 7 | mpompt 5970 |
. . . 4
      
             
                     |
9 | | nfcv 2319 |
. . . . . . 7
   |
10 | | nfmpo1 5945 |
. . . . . . 7
   
  |
11 | | nfcv 2319 |
. . . . . . 7
   |
12 | 9, 10, 11 | nfov 5908 |
. . . . . 6
          |
13 | | nfmpo1 5945 |
. . . . . . 7
   
  |
14 | 9, 13, 11 | nfov 5908 |
. . . . . 6
          |
15 | 12, 14 | nfop 3796 |
. . . . 5
                    |
16 | | nfcv 2319 |
. . . . . . 7
   |
17 | | nfmpo2 5946 |
. . . . . . 7
   
  |
18 | | nfcv 2319 |
. . . . . . 7
   |
19 | 16, 17, 18 | nfov 5908 |
. . . . . 6
          |
20 | | nfmpo2 5946 |
. . . . . . 7
   
  |
21 | 16, 20, 18 | nfov 5908 |
. . . . . 6
          |
22 | 19, 21 | nfop 3796 |
. . . . 5
                    |
23 | | nfcv 2319 |
. . . . 5
                    |
24 | | nfcv 2319 |
. . . . 5
                    |
25 | | oveq12 5887 |
. . . . . 6
 
                 |
26 | | oveq12 5887 |
. . . . . 6
 
                 |
27 | 25, 26 | opeq12d 3788 |
. . . . 5
 
                 
            
      |
28 | 15, 22, 23, 24, 27 | cbvmpo 5957 |
. . . 4
              
    
                     |
29 | 8, 28 | eqtri 2198 |
. . 3
      
             
                     |
30 | | cnmpt21.j |
. . . . 5
 TopOn    |
31 | | cnmpt21.k |
. . . . 5
 TopOn    |
32 | | txtopon 13902 |
. . . . 5
  TopOn  TopOn  
  TopOn      |
33 | 30, 31, 32 | syl2anc 411 |
. . . 4
   TopOn 
    |
34 | | toponuni 13655 |
. . . 4
   TopOn       
   |
35 | | mpteq1 4089 |
. . . 4
                                  
                |
36 | 33, 34, 35 | 3syl 17 |
. . 3
                             
                |
37 | | simp2 998 |
. . . . . 6
 

  |
38 | | simp3 999 |
. . . . . 6
 

  |
39 | | cnmpt21.a |
. . . . . . . . . . . 12
  
       |
40 | | cntop2 13842 |
. . . . . . . . . . . 12
       
  |
41 | 39, 40 | syl 14 |
. . . . . . . . . . 11
   |
42 | | toptopon2 13659 |
. . . . . . . . . . 11

TopOn     |
43 | 41, 42 | sylib 122 |
. . . . . . . . . 10
 TopOn     |
44 | | cnf2 13845 |
. . . . . . . . . 10
    TopOn 
  TopOn                       |
45 | 33, 43, 39, 44 | syl3anc 1238 |
. . . . . . . . 9
  
          |
46 | | eqid 2177 |
. . . . . . . . . 10
       |
47 | 46 | fmpo 6205 |
. . . . . . . . 9
 


            |
48 | 45, 47 | sylibr 134 |
. . . . . . . 8
  
   |
49 | | rsp2 2527 |
. . . . . . . 8
 

  

    |
50 | 48, 49 | syl 14 |
. . . . . . 7
        |
51 | 50 | 3impib 1201 |
. . . . . 6
 

   |
52 | 46 | ovmpt4g 6000 |
. . . . . 6
 
           |
53 | 37, 38, 51, 52 | syl3anc 1238 |
. . . . 5
 

   
     |
54 | | cnmpt2t.b |
. . . . . . . . . . . 12
  
       |
55 | | cntop2 13842 |
. . . . . . . . . . . 12
       
  |
56 | 54, 55 | syl 14 |
. . . . . . . . . . 11
   |
57 | | toptopon2 13659 |
. . . . . . . . . . 11

TopOn     |
58 | 56, 57 | sylib 122 |
. . . . . . . . . 10
 TopOn     |
59 | | cnf2 13845 |
. . . . . . . . . 10
    TopOn 
  TopOn                       |
60 | 33, 58, 54, 59 | syl3anc 1238 |
. . . . . . . . 9
  
          |
61 | | eqid 2177 |
. . . . . . . . . 10
       |
62 | 61 | fmpo 6205 |
. . . . . . . . 9
 


            |
63 | 60, 62 | sylibr 134 |
. . . . . . . 8
  
   |
64 | | rsp2 2527 |
. . . . . . . 8
 

  

    |
65 | 63, 64 | syl 14 |
. . . . . . 7
        |
66 | 65 | 3impib 1201 |
. . . . . 6
 

   |
67 | 61 | ovmpt4g 6000 |
. . . . . 6
 
           |
68 | 37, 38, 66, 67 | syl3anc 1238 |
. . . . 5
 

   
     |
69 | 53, 68 | opeq12d 3788 |
. . . 4
 

    
                 |
70 | 69 | mpoeq3dva 5942 |
. . 3
  
                     
    |
71 | 29, 36, 70 | 3eqtr3a 2234 |
. 2
   
                           |
72 | | eqid 2177 |
. . . 4
       |
73 | | eqid 2177 |
. . . 4
               
                     
       |
74 | 72, 73 | txcnmpt 13913 |
. . 3
   
                            
              |
75 | 39, 54, 74 | syl2anc 411 |
. 2
   
                           |
76 | 71, 75 | eqeltrrd 2255 |
1
  
            |