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

       |
6 | 2, 3, 4, 5 | syl3anc 1269 |
. . . . . . . . . . 11
         |
7 | | eqid 2453 |
. . . . . . . . . . . 12
     |
8 | 7 | fmpt 6048 |
. . . . . . . . . . 11
 
        |
9 | 6, 8 | sylibr 216 |
. . . . . . . . . 10
 
  |
10 | 9 | r19.21bi 2759 |
. . . . . . . . 9
 
   |
11 | 7 | fvmpt2 5962 |
. . . . . . . . 9
 
         |
12 | 1, 10, 11 | syl2anc 667 |
. . . . . . . 8
 
         |
13 | 12 | fveq2d 5874 |
. . . . . . 7
 
                     |
14 | | cnmpt11.b |
. . . . . . . . . . . . . 14
       |
15 | | cntop2 20269 |
. . . . . . . . . . . . . 14
    
  |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . 13
   |
17 | | eqid 2453 |
. . . . . . . . . . . . . 14
   |
18 | 17 | toptopon 19960 |
. . . . . . . . . . . . 13

TopOn     |
19 | 16, 18 | sylib 200 |
. . . . . . . . . . . 12
 TopOn     |
20 | | cnf2 20277 |
. . . . . . . . . . . 12
  TopOn  TopOn                 |
21 | 3, 19, 14, 20 | syl3anc 1269 |
. . . . . . . . . . 11
          |
22 | | eqid 2453 |
. . . . . . . . . . . 12
     |
23 | 22 | fmpt 6048 |
. . . . . . . . . . 11
 


        |
24 | 21, 23 | sylibr 216 |
. . . . . . . . . 10
 
   |
25 | 24 | adantr 467 |
. . . . . . . . 9
 
 
   |
26 | | cnmpt11.c |
. . . . . . . . . . 11
   |
27 | 26 | eleq1d 2515 |
. . . . . . . . . 10
 

    |
28 | 27 | rspcv 3148 |
. . . . . . . . 9
  

    |
29 | 10, 25, 28 | sylc 62 |
. . . . . . . 8
 
    |
30 | 26, 22 | fvmptg 5951 |
. . . . . . . 8
 
          |
31 | 10, 29, 30 | syl2anc 667 |
. . . . . . 7
 
         |
32 | 13, 31 | eqtrd 2487 |
. . . . . 6
 
               |
33 | | fvco3 5947 |
. . . . . . 7
        
                        |
34 | 6, 33 | sylan 474 |
. . . . . 6
 
                         |
35 | | eqid 2453 |
. . . . . . . 8
     |
36 | 35 | fvmpt2 5962 |
. . . . . . 7
 
          |
37 | 1, 29, 36 | syl2anc 667 |
. . . . . 6
 
         |
38 | 32, 34, 37 | 3eqtr4d 2497 |
. . . . 5
 
                   |
39 | 38 | ralrimiva 2804 |
. . . 4
                    |
40 | | nfv 1763 |
. . . . 5
                   |
41 | | nfcv 2594 |
. . . . . . . 8
     |
42 | | nfmpt1 4495 |
. . . . . . . 8
     |
43 | 41, 42 | nfco 5003 |
. . . . . . 7
         |
44 | | nfcv 2594 |
. . . . . . 7
   |
45 | 43, 44 | nffv 5877 |
. . . . . 6
             |
46 | | nfmpt1 4495 |
. . . . . . 7
     |
47 | 46, 44 | nffv 5877 |
. . . . . 6
         |
48 | 45, 47 | nfeq 2605 |
. . . . 5
                   |
49 | | fveq2 5870 |
. . . . . 6
                       |
50 | | fveq2 5870 |
. . . . . 6
               |
51 | 49, 50 | eqeq12d 2468 |
. . . . 5
                 
                   |
52 | 40, 48, 51 | cbvral 3017 |
. . . 4
 
                                   |
53 | 39, 52 | sylib 200 |
. . 3
                    |
54 | | fco 5744 |
. . . . . 6
        
                    |
55 | 21, 6, 54 | syl2anc 667 |
. . . . 5
              |
56 | | ffn 5733 |
. . . . 5
           
        |
57 | 55, 56 | syl 17 |
. . . 4
         |
58 | 29, 35 | fmptd 6051 |
. . . . 5
          |
59 | | ffn 5733 |
. . . . 5
            |
60 | 58, 59 | syl 17 |
. . . 4
     |
61 | | eqfnfv 5981 |
. . . 4
                   

                   |
62 | 57, 60, 61 | syl2anc 667 |
. . 3
         

                   |
63 | 53, 62 | mpbird 236 |
. 2
           |
64 | | cnco 20294 |
. . 3
                     |
65 | 4, 14, 64 | syl2anc 667 |
. 2
           |
66 | 63, 65 | eqeltrrd 2532 |
1
       |