Step | Hyp | Ref
| Expression |
1 | | lmcnp.4 |
. . . . . 6
         |
2 | | eqid 2462 |
. . . . . . 7
   |
3 | | eqid 2462 |
. . . . . . 7
   |
4 | 2, 3 | cnpf 20312 |
. . . . . 6
               |
5 | 1, 4 | syl 17 |
. . . . 5
         |
6 | | lmcnp.3 |
. . . . . . . . 9
          |
7 | | cnptop1 20307 |
. . . . . . . . . . . 12
         |
8 | 1, 7 | syl 17 |
. . . . . . . . . . 11
   |
9 | 2 | toptopon 19997 |
. . . . . . . . . . 11

TopOn     |
10 | 8, 9 | sylib 201 |
. . . . . . . . . 10
 TopOn     |
11 | | nnuz 11223 |
. . . . . . . . . 10
     |
12 | | 1zzd 10997 |
. . . . . . . . . 10
   |
13 | 10, 11, 12 | lmbr2 20324 |
. . . . . . . . 9
        
     

 
                |
14 | 6, 13 | mpbid 215 |
. . . . . . . 8
       
                 |
15 | 14 | simp1d 1026 |
. . . . . . 7
      |
16 | | uniexg 6615 |
. . . . . . . . 9
    |
17 | 8, 16 | syl 17 |
. . . . . . . 8
    |
18 | | cnex 9646 |
. . . . . . . 8
 |
19 | | elpm2g 7514 |
. . . . . . . 8
                  |
20 | 17, 18, 19 | sylancl 673 |
. . . . . . 7
               |
21 | 15, 20 | mpbid 215 |
. . . . . 6
          |
22 | 21 | simpld 465 |
. . . . 5
        |
23 | | fco 5762 |
. . . . 5
       
               |
24 | 5, 22, 23 | syl2anc 671 |
. . . 4
          |
25 | | fdm 5756 |
. . . . . 6
            |
26 | 24, 25 | syl 17 |
. . . . 5
     |
27 | 26 | feq2d 5737 |
. . . 4
      
   
          |
28 | 24, 27 | mpbird 240 |
. . 3
     
      |
29 | 21 | simprd 469 |
. . . 4
   |
30 | 26, 29 | eqsstrd 3478 |
. . 3
     |
31 | | cnptop2 20308 |
. . . . . 6
         |
32 | 1, 31 | syl 17 |
. . . . 5
   |
33 | | uniexg 6615 |
. . . . 5
    |
34 | 32, 33 | syl 17 |
. . . 4
    |
35 | | elpm2g 7514 |
. . . 4
               
    

    |
36 | 34, 18, 35 | sylancl 673 |
. . 3
            
    

    |
37 | 28, 30, 36 | mpbir2and 938 |
. 2
        |
38 | 14 | simp2d 1027 |
. . 3
    |
39 | 5, 38 | ffvelrnd 6046 |
. 2
        |
40 | 14 | simp3d 1028 |
. . . . . 6
  
                |
41 | 40 | adantr 471 |
. . . . 5
 

      

                |
42 | | cnpimaex 20321 |
. . . . . . 7
       
     

   
   |
43 | 42 | 3expb 1216 |
. . . . . 6
        
     


       |
44 | 1, 43 | sylan 478 |
. . . . 5
 

      

   
   |
45 | | r19.29 2937 |
. . . . . . 7
   
                      
 
              
        |
46 | | pm3.45 850 |
. . . . . . . . 9
  
                     
                    |
47 | 46 | imp 435 |
. . . . . . . 8
                                             |
48 | 47 | reximi 2867 |
. . . . . . 7
                         
                     |
49 | 45, 48 | syl 17 |
. . . . . 6
   
                      
                     |
50 | 5 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . 18
    
            
         |
51 | | ffn 5751 |
. . . . . . . . . . . . . . . . . 18
          |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . 17
    
            
    |
53 | | simplrl 775 |
. . . . . . . . . . . . . . . . . 18
    
            
   |
54 | | elssuni 4241 |
. . . . . . . . . . . . . . . . . 18
    |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
    
            
    |
56 | | fnfvima 6168 |
. . . . . . . . . . . . . . . . . 18
  
                    |
57 | 56 | 3expia 1217 |
. . . . . . . . . . . . . . . . 17
  
 
    
               |
58 | 52, 55, 57 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
    
            
     
               |
59 | 22 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . 18
                        |
60 | | fvco3 5965 |
. . . . . . . . . . . . . . . . . 18
      
                 |
61 | 59, 60 | sylan 478 |
. . . . . . . . . . . . . . . . 17
    
            
                 |
62 | 61 | eleq1d 2524 |
. . . . . . . . . . . . . . . 16
    
            
                           |
63 | 58, 62 | sylibrd 242 |
. . . . . . . . . . . . . . 15
    
            
     
 
           |
64 | | simplrr 776 |
. . . . . . . . . . . . . . . 16
    
            
       |
65 | 64 | sseld 3443 |
. . . . . . . . . . . . . . 15
    
            
           
 
       |
66 | 63, 65 | syld 45 |
. . . . . . . . . . . . . 14
    
            
     
 
       |
67 | | simpr 467 |
. . . . . . . . . . . . . . 15
    
            
   |
68 | 26 | ad3antrrr 741 |
. . . . . . . . . . . . . . 15
    
            

    |
69 | 67, 68 | eleqtrrd 2543 |
. . . . . . . . . . . . . 14
    
            
 
   |
70 | 66, 69 | jctild 550 |
. . . . . . . . . . . . 13
    
            
     
             |
71 | 70 | expimpd 612 |
. . . . . . . . . . . 12
                  
      
           |
72 | 71 | ralimdv 2810 |
. . . . . . . . . . 11
                             
       

 
        |
73 | 72 | reximdv 2873 |
. . . . . . . . . 10
                              
        

 
        |
74 | 73 | expr 624 |
. . . . . . . . 9
          
                  
        

 
         |
75 | 74 | com23 81 |
. . . . . . . 8
          
 
           
                          |
76 | 75 | impd 437 |
. . . . . . 7
          
  
                 
                   |
77 | 76 | rexlimdva 2891 |
. . . . . 6
 

                                   

 
        |
78 | 49, 77 | syl5 33 |
. . . . 5
 

        

              

                          |
79 | 41, 44, 78 | mp2and 690 |
. . . 4
 

      
                  |
80 | 79 | expr 624 |
. . 3
 
      
                   |
81 | 80 | ralrimiva 2814 |
. 2
                           |
82 | 3 | toptopon 19997 |
. . . 4

TopOn     |
83 | 32, 82 | sylib 201 |
. . 3
 TopOn     |
84 | 83, 11, 12 | lmbr2 20324 |
. 2
              
 
         
     
                     |
85 | 37, 39, 81, 84 | mpbir3and 1197 |
1
                |