Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . . . . . . . 9
 
   |
2 | | cnmptid.j |
. . . . . . . . . . . 12
 TopOn    |
3 | | cnmpt11.k |
. . . . . . . . . . . 12
 TopOn    |
4 | | cnmpt11.a |
. . . . . . . . . . . 12
       |
5 | | cnf2 13372 |
. . . . . . . . . . . 12
  TopOn  TopOn      

       |
6 | 2, 3, 4, 5 | syl3anc 1238 |
. . . . . . . . . . 11
         |
7 | | eqid 2177 |
. . . . . . . . . . . 12
     |
8 | 7 | fmpt 5662 |
. . . . . . . . . . 11
 
        |
9 | 6, 8 | sylibr 134 |
. . . . . . . . . 10
 
  |
10 | 9 | r19.21bi 2565 |
. . . . . . . . 9
 
   |
11 | 7 | fvmpt2 5595 |
. . . . . . . . 9
 
         |
12 | 1, 10, 11 | syl2anc 411 |
. . . . . . . 8
 
         |
13 | 12 | fveq2d 5515 |
. . . . . . 7
 
                     |
14 | | eqid 2177 |
. . . . . . . 8
     |
15 | | cnmpt11.c |
. . . . . . . 8
   |
16 | 15 | eleq1d 2246 |
. . . . . . . . 9
 

    |
17 | | cnmpt11.b |
. . . . . . . . . . . . . 14
       |
18 | | cntop2 13369 |
. . . . . . . . . . . . . 14
    
  |
19 | 17, 18 | syl 14 |
. . . . . . . . . . . . 13
   |
20 | | eqid 2177 |
. . . . . . . . . . . . . 14
   |
21 | 20 | toptopon 13183 |
. . . . . . . . . . . . 13

TopOn     |
22 | 19, 21 | sylib 122 |
. . . . . . . . . . . 12
 TopOn     |
23 | | cnf2 13372 |
. . . . . . . . . . . 12
  TopOn  TopOn                 |
24 | 3, 22, 17, 23 | syl3anc 1238 |
. . . . . . . . . . 11
          |
25 | 14 | fmpt 5662 |
. . . . . . . . . . 11
 


        |
26 | 24, 25 | sylibr 134 |
. . . . . . . . . 10
 
   |
27 | 26 | adantr 276 |
. . . . . . . . 9
 
 
   |
28 | 16, 27, 10 | rspcdva 2846 |
. . . . . . . 8
 
    |
29 | 14, 15, 10, 28 | fvmptd3 5605 |
. . . . . . 7
 
         |
30 | 13, 29 | eqtrd 2210 |
. . . . . 6
 
               |
31 | | fvco3 5583 |
. . . . . . 7
        
                        |
32 | 6, 31 | sylan 283 |
. . . . . 6
 
                         |
33 | | eqid 2177 |
. . . . . . . 8
     |
34 | 33 | fvmpt2 5595 |
. . . . . . 7
 
          |
35 | 1, 28, 34 | syl2anc 411 |
. . . . . 6
 
         |
36 | 30, 32, 35 | 3eqtr4d 2220 |
. . . . 5
 
                   |
37 | 36 | ralrimiva 2550 |
. . . 4
                    |
38 | | nfv 1528 |
. . . . 5
                   |
39 | | nfcv 2319 |
. . . . . . . 8
     |
40 | | nfmpt1 4093 |
. . . . . . . 8
     |
41 | 39, 40 | nfco 4788 |
. . . . . . 7
         |
42 | | nfcv 2319 |
. . . . . . 7
   |
43 | 41, 42 | nffv 5521 |
. . . . . 6
             |
44 | | nfmpt1 4093 |
. . . . . . 7
     |
45 | 44, 42 | nffv 5521 |
. . . . . 6
         |
46 | 43, 45 | nfeq 2327 |
. . . . 5
                   |
47 | | fveq2 5511 |
. . . . . 6
                       |
48 | | fveq2 5511 |
. . . . . 6
               |
49 | 47, 48 | eqeq12d 2192 |
. . . . 5
                 
                   |
50 | 38, 46, 49 | cbvral 2699 |
. . . 4
 
                                   |
51 | 37, 50 | sylib 122 |
. . 3
                    |
52 | | fco 5377 |
. . . . . 6
        
                    |
53 | 24, 6, 52 | syl2anc 411 |
. . . . 5
              |
54 | 53 | ffnd 5362 |
. . . 4
         |
55 | 28 | fmpttd 5667 |
. . . . 5
          |
56 | 55 | ffnd 5362 |
. . . 4
     |
57 | | eqfnfv 5609 |
. . . 4
                   

                   |
58 | 54, 56, 57 | syl2anc 411 |
. . 3
         

                   |
59 | 51, 58 | mpbird 167 |
. 2
           |
60 | | cnco 13388 |
. . 3
                     |
61 | 4, 17, 60 | syl2anc 411 |
. 2
           |
62 | 59, 61 | eqeltrrd 2255 |
1
       |