Proof of Theorem cnmpt22
Step | Hyp | Ref
| Expression |
1 | | df-ov 6311 |
. . . 4
   
     
        |
2 | | cnmpt21.j |
. . . . . . . . . 10
 TopOn    |
3 | | cnmpt21.k |
. . . . . . . . . 10
 TopOn    |
4 | | txtopon 20683 |
. . . . . . . . . 10
  TopOn  TopOn  
  TopOn      |
5 | 2, 3, 4 | syl2anc 673 |
. . . . . . . . 9
   TopOn 
    |
6 | | cnmpt22.l |
. . . . . . . . 9
 TopOn    |
7 | | cnmpt21.a |
. . . . . . . . 9
  
       |
8 | | cnf2 20342 |
. . . . . . . . 9
    TopOn 
  TopOn   
     
           |
9 | 5, 6, 7, 8 | syl3anc 1292 |
. . . . . . . 8
  
         |
10 | | eqid 2471 |
. . . . . . . . 9
       |
11 | 10 | fmpt2 6879 |
. . . . . . . 8
 

           |
12 | 9, 11 | sylibr 217 |
. . . . . . 7
  
  |
13 | | rsp2 2780 |
. . . . . . 7
 

 
    |
14 | 12, 13 | syl 17 |
. . . . . 6
       |
15 | 14 | 3impib 1229 |
. . . . 5
 

  |
16 | | cnmpt22.m |
. . . . . . . . 9
 TopOn    |
17 | | cnmpt2t.b |
. . . . . . . . 9
  
       |
18 | | cnf2 20342 |
. . . . . . . . 9
    TopOn 
  TopOn   
     
           |
19 | 5, 16, 17, 18 | syl3anc 1292 |
. . . . . . . 8
  
         |
20 | | eqid 2471 |
. . . . . . . . 9
       |
21 | 20 | fmpt2 6879 |
. . . . . . . 8
 

           |
22 | 19, 21 | sylibr 217 |
. . . . . . 7
  
  |
23 | | rsp2 2780 |
. . . . . . 7
 

 
    |
24 | 22, 23 | syl 17 |
. . . . . 6
       |
25 | 24 | 3impib 1229 |
. . . . 5
 

  |
26 | 15, 25 | jca 541 |
. . . . . 6
 


   |
27 | | txtopon 20683 |
. . . . . . . . . . 11
  TopOn  TopOn  
  TopOn      |
28 | 6, 16, 27 | syl2anc 673 |
. . . . . . . . . 10
   TopOn 
    |
29 | | cnmpt22.c |
. . . . . . . . . . . 12
  
       |
30 | | cntop2 20334 |
. . . . . . . . . . . 12
  
    
  |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
   |
32 | | eqid 2471 |
. . . . . . . . . . . 12
   |
33 | 32 | toptopon 20025 |
. . . . . . . . . . 11

TopOn     |
34 | 31, 33 | sylib 201 |
. . . . . . . . . 10
 TopOn     |
35 | | cnf2 20342 |
. . . . . . . . . 10
    TopOn 
  TopOn            
          |
36 | 28, 34, 29, 35 | syl3anc 1292 |
. . . . . . . . 9
  
          |
37 | | eqid 2471 |
. . . . . . . . . 10
 
     |
38 | 37 | fmpt2 6879 |
. . . . . . . . 9
 


            |
39 | 36, 38 | sylibr 217 |
. . . . . . . 8
  
   |
40 | | r2al 2783 |
. . . . . . . 8
 


           |
41 | 39, 40 | sylib 201 |
. . . . . . 7
            |
42 | 41 | 3ad2ant1 1051 |
. . . . . 6
 

           |
43 | | eleq1 2537 |
. . . . . . . . 9
 
   |
44 | | eleq1 2537 |
. . . . . . . . 9
 
   |
45 | 43, 44 | bi2anan9 890 |
. . . . . . . 8
 
   

    |
46 | | cnmpt22.d |
. . . . . . . . 9
 
   |
47 | 46 | eleq1d 2533 |
. . . . . . . 8
 
       |
48 | 45, 47 | imbi12d 327 |
. . . . . . 7
 
      
 
      |
49 | 48 | spc2gv 3123 |
. . . . . 6
 
                   |
50 | 26, 42, 26, 49 | syl3c 62 |
. . . . 5
 

   |
51 | 46, 37 | ovmpt2ga 6445 |
. . . . 5
 
     
     |
52 | 15, 25, 50, 51 | syl3anc 1292 |
. . . 4
 

   
     |
53 | 1, 52 | syl5eqr 2519 |
. . 3
 

  
         |
54 | 53 | mpt2eq3dva 6374 |
. 2
  
                |
55 | 2, 3, 7, 17 | cnmpt2t 20765 |
. . 3
  
            |
56 | 2, 3, 55, 29 | cnmpt21f 20764 |
. 2
  
                 |
57 | 54, 56 | eqeltrrd 2550 |
1
  
       |