Step | Hyp | Ref
| Expression |
1 | | df-ov 6202 |
. . . . . . . . . 10
   
              |
2 | | simprl 755 |
. . . . . . . . . . 11
 

 
  |
3 | | simprr 756 |
. . . . . . . . . . 11
 

    |
4 | | cnmpt21.j |
. . . . . . . . . . . . . . . 16
 TopOn    |
5 | | cnmpt21.k |
. . . . . . . . . . . . . . . 16
 TopOn    |
6 | | txtopon 19295 |
. . . . . . . . . . . . . . . 16
  TopOn  TopOn  
  TopOn      |
7 | 4, 5, 6 | syl2anc 661 |
. . . . . . . . . . . . . . 15
   TopOn 
    |
8 | | cnmpt21.l |
. . . . . . . . . . . . . . 15
 TopOn    |
9 | | cnmpt21.a |
. . . . . . . . . . . . . . 15
  
       |
10 | | cnf2 18984 |
. . . . . . . . . . . . . . 15
    TopOn 
  TopOn   
     
           |
11 | 7, 8, 9, 10 | syl3anc 1219 |
. . . . . . . . . . . . . 14
  
         |
12 | | eqid 2454 |
. . . . . . . . . . . . . . 15
       |
13 | 12 | fmpt2 6750 |
. . . . . . . . . . . . . 14
 

           |
14 | 11, 13 | sylibr 212 |
. . . . . . . . . . . . 13
  
  |
15 | | rsp2 2894 |
. . . . . . . . . . . . 13
 

 
    |
16 | 14, 15 | syl 16 |
. . . . . . . . . . . 12
       |
17 | 16 | imp 429 |
. . . . . . . . . . 11
 

 
  |
18 | 12 | ovmpt4g 6322 |
. . . . . . . . . . 11
 
          |
19 | 2, 3, 17, 18 | syl3anc 1219 |
. . . . . . . . . 10
 

           |
20 | 1, 19 | syl5eqr 2509 |
. . . . . . . . 9
 

              |
21 | 20 | fveq2d 5802 |
. . . . . . . 8
 

                          |
22 | | cnmpt21.b |
. . . . . . . . . . . . . . 15
       |
23 | | cntop2 18976 |
. . . . . . . . . . . . . . 15
    
  |
24 | 22, 23 | syl 16 |
. . . . . . . . . . . . . 14
   |
25 | | eqid 2454 |
. . . . . . . . . . . . . . 15
   |
26 | 25 | toptopon 18669 |
. . . . . . . . . . . . . 14

TopOn     |
27 | 24, 26 | sylib 196 |
. . . . . . . . . . . . 13
 TopOn     |
28 | | cnf2 18984 |
. . . . . . . . . . . . 13
  TopOn  TopOn                 |
29 | 8, 27, 22, 28 | syl3anc 1219 |
. . . . . . . . . . . 12
          |
30 | | eqid 2454 |
. . . . . . . . . . . . 13
     |
31 | 30 | fmpt 5972 |
. . . . . . . . . . . 12
 


        |
32 | 29, 31 | sylibr 212 |
. . . . . . . . . . 11
 
   |
33 | 32 | adantr 465 |
. . . . . . . . . 10
 

  
   |
34 | | cnmpt21.c |
. . . . . . . . . . . 12
   |
35 | 34 | eleq1d 2523 |
. . . . . . . . . . 11
 

    |
36 | 35 | rspcv 3173 |
. . . . . . . . . 10
  

    |
37 | 17, 33, 36 | sylc 60 |
. . . . . . . . 9
 

 
   |
38 | 34, 30 | fvmptg 5880 |
. . . . . . . . 9
 
          |
39 | 17, 37, 38 | syl2anc 661 |
. . . . . . . 8
 

          |
40 | 21, 39 | eqtrd 2495 |
. . . . . . 7
 

                    |
41 | | opelxpi 4978 |
. . . . . . . 8
 
        |
42 | | fvco3 5876 |
. . . . . . . 8
   
            
                                |
43 | 11, 41, 42 | syl2an 477 |
. . . . . . 7
 

               
       
          |
44 | | df-ov 6202 |
. . . . . . . 8
   
              |
45 | | eqid 2454 |
. . . . . . . . . 10
       |
46 | 45 | ovmpt4g 6322 |
. . . . . . . . 9
 
           |
47 | 2, 3, 37, 46 | syl3anc 1219 |
. . . . . . . 8
 

           |
48 | 44, 47 | syl5eqr 2509 |
. . . . . . 7
 

              |
49 | 40, 43, 48 | 3eqtr4d 2505 |
. . . . . 6
 

               
  
         |
50 | 49 | ralrimivva 2912 |
. . . . 5
  
             
  
         |
51 | | nfv 1674 |
. . . . . 6
  
             
  
        |
52 | | nfcv 2616 |
. . . . . . 7
   |
53 | | nfcv 2616 |
. . . . . . . . . 10
     |
54 | | nfmpt21 6261 |
. . . . . . . . . 10
   
  |
55 | 53, 54 | nfco 5112 |
. . . . . . . . 9
      
   |
56 | | nfcv 2616 |
. . . . . . . . 9
      |
57 | 55, 56 | nffv 5805 |
. . . . . . . 8
                 |
58 | | nfmpt21 6261 |
. . . . . . . . 9
   
  |
59 | 58, 56 | nffv 5805 |
. . . . . . . 8
             |
60 | 57, 59 | nfeq 2626 |
. . . . . . 7
               
  
        |
61 | 52, 60 | nfral 2886 |
. . . . . 6
  
             
  
        |
62 | | nfv 1674 |
. . . . . . . 8
               
  
        |
63 | | nfcv 2616 |
. . . . . . . . . . 11
     |
64 | | nfmpt22 6262 |
. . . . . . . . . . 11
   
  |
65 | 63, 64 | nfco 5112 |
. . . . . . . . . 10
      
   |
66 | | nfcv 2616 |
. . . . . . . . . 10
      |
67 | 65, 66 | nffv 5805 |
. . . . . . . . 9
                 |
68 | | nfmpt22 6262 |
. . . . . . . . . 10
   
  |
69 | 68, 66 | nffv 5805 |
. . . . . . . . 9
             |
70 | 67, 69 | nfeq 2626 |
. . . . . . . 8
               
  
        |
71 | | opeq2 4167 |
. . . . . . . . . 10
         |
72 | 71 | fveq2d 5802 |
. . . . . . . . 9
      
                        |
73 | 71 | fveq2d 5802 |
. . . . . . . . 9
   
                   |
74 | 72, 73 | eqeq12d 2476 |
. . . . . . . 8
               
  
            
                     |
75 | 62, 70, 74 | cbvral 3047 |
. . . . . . 7
 
     
                        
                    |
76 | | opeq1 4166 |
. . . . . . . . . 10
         |
77 | 76 | fveq2d 5802 |
. . . . . . . . 9
      
                        |
78 | 76 | fveq2d 5802 |
. . . . . . . . 9
   
                   |
79 | 77, 78 | eqeq12d 2476 |
. . . . . . . 8
               
  
            
                     |
80 | 79 | ralbidv 2845 |
. . . . . . 7
  
             
  
             
                     |
81 | 75, 80 | syl5bb 257 |
. . . . . 6
  
             
  
             
                     |
82 | 51, 61, 81 | cbvral 3047 |
. . . . 5
 

     
                   
     
                    |
83 | 50, 82 | sylib 196 |
. . . 4
  
             
  
         |
84 | | fveq2 5798 |
. . . . . 6
                               |
85 | | fveq2 5798 |
. . . . . 6
                       |
86 | 84, 85 | eqeq12d 2476 |
. . . . 5
                                    
  
          |
87 | 86 | ralxp 5088 |
. . . 4
 
                     

             
  
         |
88 | 83, 87 | sylibr 212 |
. . 3
                         |
89 | | fco 5675 |
. . . . . 6
        
         
                |
90 | 29, 11, 89 | syl2anc 661 |
. . . . 5
     
           |
91 | | ffn 5666 |
. . . . 5
                          |
92 | 90, 91 | syl 16 |
. . . 4
     
      |
93 | 37 | ralrimivva 2912 |
. . . . . 6
  
   |
94 | 45 | fmpt2 6750 |
. . . . . 6
 


            |
95 | 93, 94 | sylib 196 |
. . . . 5
  
          |
96 | | ffn 5666 |
. . . . 5
          
       |
97 | 95, 96 | syl 16 |
. . . 4
  
     |
98 | | eqfnfv 5905 |
. . . 4
      
   
           
   

                         |
99 | 92, 97, 98 | syl2anc 661 |
. . 3
           
                         |
100 | 88, 99 | mpbird 232 |
. 2
     
   
   |
101 | | cnco 19001 |
. . 3
   
                       |
102 | 9, 22, 101 | syl2anc 661 |
. 2
     
        |
103 | 100, 102 | eqeltrrd 2543 |
1
  
       |