Step | Hyp | Ref
| Expression |
1 | | metcn.2 |
. . . . 5
     |
2 | 1 | mopntopon 12371 |
. . . 4
      TopOn    |
3 | 2 | 3ad2ant1 970 |
. . 3
           
 TopOn    |
4 | | metcn.4 |
. . . . 5
     |
5 | 4 | mopnval 12370 |
. . . 4
                |
6 | 5 | 3ad2ant2 971 |
. . 3
           
           |
7 | 4 | mopntopon 12371 |
. . . 4
      TopOn    |
8 | 7 | 3ad2ant2 971 |
. . 3
           
 TopOn    |
9 | | simp3 951 |
. . 3
           
   |
10 | 3, 6, 8, 9 | tgcnp 12159 |
. 2
           
 
     
     
          

          |
11 | | simpll2 989 |
. . . . . . . 8
                   

       |
12 | | simplr 500 |
. . . . . . . . 9
                   
       |
13 | | simpll3 990 |
. . . . . . . . 9
                   

  |
14 | 12, 13 | ffvelrnd 5488 |
. . . . . . . 8
                   
       |
15 | | simpr 109 |
. . . . . . . 8
                   
   |
16 | | blcntr 12344 |
. . . . . . . 8
          
                   |
17 | 11, 14, 15, 16 | syl3anc 1184 |
. . . . . . 7
                   
                   |
18 | | rpxr 9298 |
. . . . . . . . . 10

  |
19 | 18 | adantl 273 |
. . . . . . . . 9
                   
   |
20 | | blelrn 12348 |
. . . . . . . . 9
          
                   |
21 | 11, 14, 19, 20 | syl3anc 1184 |
. . . . . . . 8
                   
                   |
22 | | eleq2 2163 |
. . . . . . . . . 10
                 
                   |
23 | | sseq2 3071 |
. . . . . . . . . . . 12
                 
                   |
24 | 23 | anbi2d 455 |
. . . . . . . . . . 11
                                         |
25 | 24 | rexbidv 2397 |
. . . . . . . . . 10
              

   
                       |
26 | 22, 25 | imbi12d 233 |
. . . . . . . . 9
                    
   
                    
   
                 |
27 | 26 | rspcv 2740 |
. . . . . . . 8
                
 
          

                       

   
                 |
28 | 21, 27 | syl 14 |
. . . . . . 7
                   
            


                       

   
                 |
29 | 17, 28 | mpid 42 |
. . . . . 6
                   
            


      

   
                |
30 | | simpl1 952 |
. . . . . . . . . . . 12
       
    
     
       |
31 | 30 | ad2antrr 475 |
. . . . . . . . . . 11
                                |
32 | | simplrr 506 |
. . . . . . . . . . 11
                           |
33 | | simpr 109 |
. . . . . . . . . . 11
                           |
34 | 1 | mopni2 12411 |
. . . . . . . . . . 11
      

           |
35 | 31, 32, 33, 34 | syl3anc 1184 |
. . . . . . . . . 10
                                    |
36 | | sstr2 3054 |
. . . . . . . . . . . 12
                     
                                       |
37 | | imass2 4851 |
. . . . . . . . . . . 12
                    
      |
38 | 36, 37 | syl11 31 |
. . . . . . . . . . 11
                                                     |
39 | 38 | reximdv 2492 |
. . . . . . . . . 10
                  
                                    |
40 | 35, 39 | syl5com 29 |
. . . . . . . . 9
                             
                        
               |
41 | 40 | expimpd 358 |
. . . . . . . 8
                      
 
                 
                           |
42 | 41 | expr 370 |
. . . . . . 7
                   
                    
            
                |
43 | 42 | rexlimdv 2507 |
. . . . . 6
                   
                    
            
               |
44 | 29, 43 | syld 45 |
. . . . 5
                   
            


      
                           |
45 | 44 | ralrimdva 2471 |
. . . 4
       
    
                 


      
            
               |
46 | | simpl2 953 |
. . . . . . . . 9
       
    
     
       |
47 | | blss 12356 |
. . . . . . . . . 10
                               |
48 | 47 | 3expib 1152 |
. . . . . . . . 9
                                 |
49 | 46, 48 | syl 14 |
. . . . . . . 8
       
    
           
    
                |
50 | | r19.29r 2529 |
. . . . . . . . . 10
               
            
             
             
                           |
51 | 30 | ad3antrrr 479 |
. . . . . . . . . . . . . . . 16
               
     
                                                |
52 | 13 | ad2antrr 475 |
. . . . . . . . . . . . . . . 16
               
     
                                           |
53 | | rpxr 9298 |
. . . . . . . . . . . . . . . . 17

  |
54 | 53 | ad2antrl 477 |
. . . . . . . . . . . . . . . 16
               
     
                                           |
55 | 1 | blopn 12418 |
. . . . . . . . . . . . . . . 16
      
           |
56 | 51, 52, 54, 55 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
               
     
                                                   |
57 | | simprl 501 |
. . . . . . . . . . . . . . . 16
               
     
                                           |
58 | | blcntr 12344 |
. . . . . . . . . . . . . . . 16
      
           |
59 | 51, 52, 57, 58 | syl3anc 1184 |
. . . . . . . . . . . . . . 15
               
     
                                                   |
60 | | sstr 3055 |
. . . . . . . . . . . . . . . . 17
                                                     |
61 | 60 | ad2ant2l 495 |
. . . . . . . . . . . . . . . 16
                                         
     
                          
  |
62 | 61 | ancoms 266 |
. . . . . . . . . . . . . . 15
               
     
                                                    
  |
63 | | eleq2 2163 |
. . . . . . . . . . . . . . . . 17
         
           |
64 | | imaeq2 4813 |
. . . . . . . . . . . . . . . . . 18
                           |
65 | 64 | sseq1d 3076 |
. . . . . . . . . . . . . . . . 17
             
           
   |
66 | 63, 65 | anbi12d 460 |
. . . . . . . . . . . . . . . 16
                                    
    |
67 | 66 | rspcev 2744 |
. . . . . . . . . . . . . . 15
          
                      

   
   |
68 | 56, 59, 62, 67 | syl12anc 1182 |
. . . . . . . . . . . . . 14
               
     
                                          
   
   |
69 | 68 | expr 370 |
. . . . . . . . . . . . 13
               
     
             
             
            

        |
70 | 69 | rexlimdva 2508 |
. . . . . . . . . . . 12
                    
                                        

        |
71 | 70 | expimpd 358 |
. . . . . . . . . . 11
                   
                                         

   
    |
72 | 71 | rexlimdva 2508 |
. . . . . . . . . 10
       
    
                                               

   
    |
73 | 50, 72 | syl5 32 |
. . . . . . . . 9
       
    
                                               


        |
74 | 73 | expd 256 |
. . . . . . . 8
       
    
                     
            
            

         |
75 | 49, 74 | syld 45 |
. . . . . . 7
       
    
           
    
 
            
            

         |
76 | 75 | com23 78 |
. . . . . 6
       
    
                                             
   
     |
77 | 76 | exp4a 361 |
. . . . 5
       
    
                                            
   
      |
78 | 77 | ralrimdv 2470 |
. . . 4
       
    
                                           


         |
79 | 45, 78 | impbid 128 |
. . 3
       
    
                 


     
                             |
80 | 79 | pm5.32da 443 |
. 2
           
                 


                                          |
81 | 10, 80 | bitrd 187 |
1
           
 
     
     
            
                |