Step | Hyp | Ref
| Expression |
1 | | fveq2 5865 |
. . . . . . 7
                       |
2 | | df-ov 6293 |
. . . . . . 7
   
              |
3 | 1, 2 | syl6eqr 2503 |
. . . . . 6
                    |
4 | | fveq2 5865 |
. . . . . . 7
                       |
5 | | df-ov 6293 |
. . . . . . 7
   
              |
6 | 4, 5 | syl6eqr 2503 |
. . . . . 6
                    |
7 | 3, 6 | opeq12d 4174 |
. . . . 5
                                 
      |
8 | 7 | mpt2mpt 6388 |
. . . 4
      
             
                     |
9 | | nfcv 2592 |
. . . . . . 7
   |
10 | | nfmpt21 6358 |
. . . . . . 7
   
  |
11 | | nfcv 2592 |
. . . . . . 7
   |
12 | 9, 10, 11 | nfov 6316 |
. . . . . 6
          |
13 | | nfmpt21 6358 |
. . . . . . 7
   
  |
14 | 9, 13, 11 | nfov 6316 |
. . . . . 6
          |
15 | 12, 14 | nfop 4182 |
. . . . 5
                    |
16 | | nfcv 2592 |
. . . . . . 7
   |
17 | | nfmpt22 6359 |
. . . . . . 7
   
  |
18 | | nfcv 2592 |
. . . . . . 7
   |
19 | 16, 17, 18 | nfov 6316 |
. . . . . 6
          |
20 | | nfmpt22 6359 |
. . . . . . 7
   
  |
21 | 16, 20, 18 | nfov 6316 |
. . . . . 6
          |
22 | 19, 21 | nfop 4182 |
. . . . 5
                    |
23 | | nfcv 2592 |
. . . . 5
                    |
24 | | nfcv 2592 |
. . . . 5
                    |
25 | | oveq12 6299 |
. . . . . 6
 
                 |
26 | | oveq12 6299 |
. . . . . 6
 
                 |
27 | 25, 26 | opeq12d 4174 |
. . . . 5
 
                 
            
      |
28 | 15, 22, 23, 24, 27 | cbvmpt2 6370 |
. . . 4
              
    
                     |
29 | 8, 28 | eqtri 2473 |
. . 3
      
             
                     |
30 | | cnmpt21.j |
. . . . 5
 TopOn    |
31 | | cnmpt21.k |
. . . . 5
 TopOn    |
32 | | txtopon 20606 |
. . . . 5
  TopOn  TopOn  
  TopOn      |
33 | 30, 31, 32 | syl2anc 667 |
. . . 4
   TopOn 
    |
34 | | toponuni 19942 |
. . . 4
   TopOn       
   |
35 | | mpteq1 4483 |
. . . 4
                                  
                |
36 | 33, 34, 35 | 3syl 18 |
. . 3
                             
                |
37 | | simp2 1009 |
. . . . . 6
 

  |
38 | | simp3 1010 |
. . . . . 6
 

  |
39 | | cnmpt21.a |
. . . . . . . . . . . 12
  
       |
40 | | cntop2 20257 |
. . . . . . . . . . . 12
       
  |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
   |
42 | | eqid 2451 |
. . . . . . . . . . . 12
   |
43 | 42 | toptopon 19948 |
. . . . . . . . . . 11

TopOn     |
44 | 41, 43 | sylib 200 |
. . . . . . . . . 10
 TopOn     |
45 | | cnf2 20265 |
. . . . . . . . . 10
    TopOn 
  TopOn                       |
46 | 33, 44, 39, 45 | syl3anc 1268 |
. . . . . . . . 9
  
          |
47 | | eqid 2451 |
. . . . . . . . . 10
       |
48 | 47 | fmpt2 6860 |
. . . . . . . . 9
 


            |
49 | 46, 48 | sylibr 216 |
. . . . . . . 8
  
   |
50 | | rsp2 2762 |
. . . . . . . 8
 

  

    |
51 | 49, 50 | syl 17 |
. . . . . . 7
        |
52 | 51 | 3impib 1206 |
. . . . . 6
 

   |
53 | 47 | ovmpt4g 6419 |
. . . . . 6
 
           |
54 | 37, 38, 52, 53 | syl3anc 1268 |
. . . . 5
 

   
     |
55 | | cnmpt2t.b |
. . . . . . . . . . . 12
  
       |
56 | | cntop2 20257 |
. . . . . . . . . . . 12
       
  |
57 | 55, 56 | syl 17 |
. . . . . . . . . . 11
   |
58 | | eqid 2451 |
. . . . . . . . . . . 12
   |
59 | 58 | toptopon 19948 |
. . . . . . . . . . 11

TopOn     |
60 | 57, 59 | sylib 200 |
. . . . . . . . . 10
 TopOn     |
61 | | cnf2 20265 |
. . . . . . . . . 10
    TopOn 
  TopOn                       |
62 | 33, 60, 55, 61 | syl3anc 1268 |
. . . . . . . . 9
  
          |
63 | | eqid 2451 |
. . . . . . . . . 10
       |
64 | 63 | fmpt2 6860 |
. . . . . . . . 9
 


            |
65 | 62, 64 | sylibr 216 |
. . . . . . . 8
  
   |
66 | | rsp2 2762 |
. . . . . . . 8
 

  

    |
67 | 65, 66 | syl 17 |
. . . . . . 7
        |
68 | 67 | 3impib 1206 |
. . . . . 6
 

   |
69 | 63 | ovmpt4g 6419 |
. . . . . 6
 
           |
70 | 37, 38, 68, 69 | syl3anc 1268 |
. . . . 5
 

   
     |
71 | 54, 70 | opeq12d 4174 |
. . . 4
 

    
                 |
72 | 71 | mpt2eq3dva 6355 |
. . 3
  
                     
    |
73 | 29, 36, 72 | 3eqtr3a 2509 |
. 2
   
                           |
74 | | eqid 2451 |
. . . 4
       |
75 | | eqid 2451 |
. . . 4
               
                     
       |
76 | 74, 75 | txcnmpt 20639 |
. . 3
   
                            
              |
77 | 39, 55, 76 | syl2anc 667 |
. 2
   
                           |
78 | 73, 77 | eqeltrrd 2530 |
1
  
            |