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

TopOn     |
5 | 3, 4 | sylib 121 |
. . . . . 6
 TopOn     |
6 | | lmcnp.k |
. . . . . . 7
   |
7 | | toptopon2 11968 |
. . . . . . 7

TopOn     |
8 | 6, 7 | sylib 121 |
. . . . . 6
 TopOn     |
9 | | lmcnp.4 |
. . . . . 6
         |
10 | | cnpf2 12157 |
. . . . . 6
  TopOn   TopOn         
        |
11 | 5, 8, 9, 10 | syl3anc 1184 |
. . . . 5
         |
12 | | nnuz 9211 |
. . . . . . . . . 10
     |
13 | | 1zzd 8933 |
. . . . . . . . . 10
   |
14 | 5, 12, 13 | lmbr2 12164 |
. . . . . . . . 9
        
     

 
                |
15 | 1, 14 | mpbid 146 |
. . . . . . . 8
       
                 |
16 | 15 | simp1d 961 |
. . . . . . 7
      |
17 | | uniexg 4299 |
. . . . . . . . 9
    |
18 | 3, 17 | syl 14 |
. . . . . . . 8
    |
19 | | cnex 7616 |
. . . . . . . 8
 |
20 | | elpm2g 6489 |
. . . . . . . 8
                  |
21 | 18, 19, 20 | sylancl 407 |
. . . . . . 7
               |
22 | 16, 21 | mpbid 146 |
. . . . . 6
          |
23 | 22 | simpld 111 |
. . . . 5
        |
24 | | fco 5224 |
. . . . 5
       
               |
25 | 11, 23, 24 | syl2anc 406 |
. . . 4
          |
26 | 25 | fdmd 5215 |
. . . . 5
     |
27 | 26 | feq2d 5196 |
. . . 4
      
   
          |
28 | 25, 27 | mpbird 166 |
. . 3
     
      |
29 | 22 | simprd 113 |
. . . 4
   |
30 | 26, 29 | eqsstrd 3083 |
. . 3
     |
31 | | uniexg 4299 |
. . . . 5
    |
32 | 6, 31 | syl 14 |
. . . 4
    |
33 | | elpm2g 6489 |
. . . 4
               
    

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

    |
35 | 28, 30, 34 | mpbir2and 896 |
. 2
        |
36 | 15 | simp2d 962 |
. . 3
    |
37 | 11, 36 | ffvelrnd 5488 |
. 2
        |
38 | 15 | simp3d 963 |
. . . . . 6
  
                |
39 | 38 | adantr 272 |
. . . . 5
 

      

                |
40 | 5 | adantr 272 |
. . . . . 6
 

     
TopOn     |
41 | 8 | adantr 272 |
. . . . . 6
 

     
TopOn     |
42 | 36 | adantr 272 |
. . . . . 6
 

     
   |
43 | 9 | adantr 272 |
. . . . . 6
 

     
        |
44 | | simprl 501 |
. . . . . 6
 

     
  |
45 | | simprr 502 |
. . . . . 6
 

            |
46 | | icnpimaex 12161 |
. . . . . 6
   TopOn  
TopOn     
     
     


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

      

   
   |
48 | | r19.29 2528 |
. . . . . . 7
   
                      
 
              
        |
49 | | pm3.45 567 |
. . . . . . . . 9
  
                     
                    |
50 | 49 | imp 123 |
. . . . . . . 8
                                             |
51 | 50 | reximi 2488 |
. . . . . . 7
                         
                     |
52 | 48, 51 | syl 14 |
. . . . . 6
   
                      
                     |
53 | 11 | ad3antrrr 479 |
. . . . . . . . . . . . . . . . . 18
    
            
         |
54 | 53 | ffnd 5209 |
. . . . . . . . . . . . . . . . 17
    
            
    |
55 | | simplrl 505 |
. . . . . . . . . . . . . . . . . 18
    
            
   |
56 | | elssuni 3711 |
. . . . . . . . . . . . . . . . . 18
    |
57 | 55, 56 | syl 14 |
. . . . . . . . . . . . . . . . 17
    
            
    |
58 | | fnfvima 5584 |
. . . . . . . . . . . . . . . . . 18
  
                    |
59 | 58 | 3expia 1151 |
. . . . . . . . . . . . . . . . 17
  
 
    
               |
60 | 54, 57, 59 | syl2anc 406 |
. . . . . . . . . . . . . . . 16
    
            
     
               |
61 | 23 | ad2antrr 475 |
. . . . . . . . . . . . . . . . . 18
                        |
62 | | fvco3 5424 |
. . . . . . . . . . . . . . . . . 18
      
                 |
63 | 61, 62 | sylan 279 |
. . . . . . . . . . . . . . . . 17
    
            
                 |
64 | 63 | eleq1d 2168 |
. . . . . . . . . . . . . . . 16
    
            
                           |
65 | 60, 64 | sylibrd 168 |
. . . . . . . . . . . . . . 15
    
            
     
 
           |
66 | | simplrr 506 |
. . . . . . . . . . . . . . . 16
    
            
       |
67 | 66 | sseld 3046 |
. . . . . . . . . . . . . . 15
    
            
           
 
       |
68 | 65, 67 | syld 45 |
. . . . . . . . . . . . . 14
    
            
     
 
       |
69 | | simpr 109 |
. . . . . . . . . . . . . . 15
    
            
   |
70 | 26 | ad3antrrr 479 |
. . . . . . . . . . . . . . 15
    
            

    |
71 | 69, 70 | eleqtrrd 2179 |
. . . . . . . . . . . . . 14
    
            
 
   |
72 | 68, 71 | jctild 312 |
. . . . . . . . . . . . 13
    
            
     
             |
73 | 72 | expimpd 358 |
. . . . . . . . . . . 12
                  
      
           |
74 | 73 | ralimdv 2459 |
. . . . . . . . . . 11
                             
       

 
        |
75 | 74 | reximdv 2492 |
. . . . . . . . . 10
                              
        

 
        |
76 | 75 | expr 370 |
. . . . . . . . 9
          
                  
        

 
         |
77 | 76 | com23 78 |
. . . . . . . 8
          
 
           
                          |
78 | 77 | impd 252 |
. . . . . . 7
          
  
                 
                   |
79 | 78 | rexlimdva 2508 |
. . . . . 6
 

                                   

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

        

              

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

      
                  |
82 | 81 | expr 370 |
. . 3
 
      
                   |
83 | 82 | ralrimiva 2464 |
. 2
                           |
84 | 8, 12, 13 | lmbr2 12164 |
. 2
              
 
         
     
                     |
85 | 35, 37, 83, 84 | mpbir3and 1132 |
1
                |