Step | Hyp | Ref
| Expression |
1 | | lmcnp.3 |
. . . . . . . 8
          |
2 | | lmrcl 13661 |
. . . . . . . 8
          |
3 | 1, 2 | syl 14 |
. . . . . . 7
   |
4 | | toptopon2 13489 |
. . . . . . 7

TopOn     |
5 | 3, 4 | sylib 122 |
. . . . . 6
 TopOn     |
6 | | lmcnp.k |
. . . . . . 7
   |
7 | | toptopon2 13489 |
. . . . . . 7

TopOn     |
8 | 6, 7 | sylib 122 |
. . . . . 6
 TopOn     |
9 | | lmcnp.4 |
. . . . . 6
         |
10 | | cnpf2 13677 |
. . . . . 6
  TopOn   TopOn         
        |
11 | 5, 8, 9, 10 | syl3anc 1238 |
. . . . 5
         |
12 | | nnuz 9562 |
. . . . . . . . . 10
     |
13 | | 1zzd 9279 |
. . . . . . . . . 10
   |
14 | 5, 12, 13 | lmbr2 13684 |
. . . . . . . . 9
        
     

 
                |
15 | 1, 14 | mpbid 147 |
. . . . . . . 8
       
                 |
16 | 15 | simp1d 1009 |
. . . . . . 7
      |
17 | | uniexg 4439 |
. . . . . . . . 9
    |
18 | 3, 17 | syl 14 |
. . . . . . . 8
    |
19 | | cnex 7934 |
. . . . . . . 8
 |
20 | | elpm2g 6664 |
. . . . . . . 8
                  |
21 | 18, 19, 20 | sylancl 413 |
. . . . . . 7
               |
22 | 16, 21 | mpbid 147 |
. . . . . 6
          |
23 | 22 | simpld 112 |
. . . . 5
        |
24 | | fco 5381 |
. . . . 5
       
               |
25 | 11, 23, 24 | syl2anc 411 |
. . . 4
          |
26 | 25 | fdmd 5372 |
. . . . 5
     |
27 | 26 | feq2d 5353 |
. . . 4
      
   
          |
28 | 25, 27 | mpbird 167 |
. . 3
     
      |
29 | 22 | simprd 114 |
. . . 4
   |
30 | 26, 29 | eqsstrd 3191 |
. . 3
     |
31 | | uniexg 4439 |
. . . . 5
    |
32 | 6, 31 | syl 14 |
. . . 4
    |
33 | | elpm2g 6664 |
. . . 4
               
    

    |
34 | 32, 19, 33 | sylancl 413 |
. . 3
            
    

    |
35 | 28, 30, 34 | mpbir2and 944 |
. 2
        |
36 | 15 | simp2d 1010 |
. . 3
    |
37 | 11, 36 | ffvelcdmd 5652 |
. 2
        |
38 | 15 | simp3d 1011 |
. . . . . 6
  
                |
39 | 38 | adantr 276 |
. . . . 5
 

      

                |
40 | 5 | adantr 276 |
. . . . . 6
 

     
TopOn     |
41 | 8 | adantr 276 |
. . . . . 6
 

     
TopOn     |
42 | 36 | adantr 276 |
. . . . . 6
 

     
   |
43 | 9 | adantr 276 |
. . . . . 6
 

     
        |
44 | | simprl 529 |
. . . . . 6
 

     
  |
45 | | simprr 531 |
. . . . . 6
 

            |
46 | | icnpimaex 13681 |
. . . . . 6
   TopOn  
TopOn     
     
     


       |
47 | 40, 41, 42, 43, 44, 45, 46 | syl33anc 1253 |
. . . . 5
 

      

   
   |
48 | | r19.29 2614 |
. . . . . . 7
   
                      
 
              
        |
49 | | pm3.45 597 |
. . . . . . . . 9
  
                     
                    |
50 | 49 | imp 124 |
. . . . . . . 8
                                             |
51 | 50 | reximi 2574 |
. . . . . . 7
                         
                     |
52 | 48, 51 | syl 14 |
. . . . . 6
   
                      
                     |
53 | 11 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . 18
    
            
         |
54 | 53 | ffnd 5366 |
. . . . . . . . . . . . . . . . 17
    
            
    |
55 | | simplrl 535 |
. . . . . . . . . . . . . . . . . 18
    
            
   |
56 | | elssuni 3837 |
. . . . . . . . . . . . . . . . . 18
    |
57 | 55, 56 | syl 14 |
. . . . . . . . . . . . . . . . 17
    
            
    |
58 | | fnfvima 5751 |
. . . . . . . . . . . . . . . . . 18
  
                    |
59 | 58 | 3expia 1205 |
. . . . . . . . . . . . . . . . 17
  
 
    
               |
60 | 54, 57, 59 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
    
            
     
               |
61 | 23 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
                        |
62 | | fvco3 5587 |
. . . . . . . . . . . . . . . . . 18
      
                 |
63 | 61, 62 | sylan 283 |
. . . . . . . . . . . . . . . . 17
    
            
                 |
64 | 63 | eleq1d 2246 |
. . . . . . . . . . . . . . . 16
    
            
                           |
65 | 60, 64 | sylibrd 169 |
. . . . . . . . . . . . . . 15
    
            
     
 
           |
66 | | simplrr 536 |
. . . . . . . . . . . . . . . 16
    
            
       |
67 | 66 | sseld 3154 |
. . . . . . . . . . . . . . 15
    
            
           
 
       |
68 | 65, 67 | syld 45 |
. . . . . . . . . . . . . 14
    
            
     
 
       |
69 | | simpr 110 |
. . . . . . . . . . . . . . 15
    
            
   |
70 | 26 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
    
            

    |
71 | 69, 70 | eleqtrrd 2257 |
. . . . . . . . . . . . . 14
    
            
 
   |
72 | 68, 71 | jctild 316 |
. . . . . . . . . . . . 13
    
            
     
             |
73 | 72 | expimpd 363 |
. . . . . . . . . . . 12
                  
      
           |
74 | 73 | ralimdv 2545 |
. . . . . . . . . . 11
                             
       

 
        |
75 | 74 | reximdv 2578 |
. . . . . . . . . 10
                              
        

 
        |
76 | 75 | expr 375 |
. . . . . . . . 9
          
                  
        

 
         |
77 | 76 | com23 78 |
. . . . . . . 8
          
 
           
                          |
78 | 77 | impd 254 |
. . . . . . 7
          
  
                 
                   |
79 | 78 | rexlimdva 2594 |
. . . . . 6
 

                                   

 
        |
80 | 52, 79 | syl5 32 |
. . . . 5
 

        

              

                          |
81 | 39, 47, 80 | mp2and 433 |
. . . 4
 

      
                  |
82 | 81 | expr 375 |
. . 3
 
      
                   |
83 | 82 | ralrimiva 2550 |
. 2
                           |
84 | 8, 12, 13 | lmbr2 13684 |
. 2
              
 
         
     
                     |
85 | 35, 37, 83, 84 | mpbir3and 1180 |
1
                |