Step | Hyp | Ref
| Expression |
1 | | simplrl 535 |
. . . . . . . 8
    TopOn 
TopOn                       |
2 | | simpll3 1038 |
. . . . . . . . 9
    TopOn 
TopOn                  
  |
3 | | snidg 3623 |
. . . . . . . . 9
     |
4 | 2, 3 | syl 14 |
. . . . . . . 8
    TopOn 
TopOn                  
    |
5 | | simprr 531 |
. . . . . . . . . 10
    TopOn 
TopOn                         |
6 | | simplrr 536 |
. . . . . . . . . . 11
    TopOn 
TopOn                         |
7 | | ffn 5367 |
. . . . . . . . . . 11
       |
8 | | elpreima 5637 |
. . . . . . . . . . 11
 
    

        |
9 | 6, 7, 8 | 3syl 17 |
. . . . . . . . . 10
    TopOn 
TopOn                                  |
10 | 2, 5, 9 | mpbir2and 944 |
. . . . . . . . 9
    TopOn 
TopOn                  
       |
11 | 10 | snssd 3739 |
. . . . . . . 8
    TopOn 
TopOn                            |
12 | | eleq2 2241 |
. . . . . . . . . 10
         |
13 | | sseq1 3180 |
. . . . . . . . . 10
                   |
14 | 12, 13 | anbi12d 473 |
. . . . . . . . 9
          
              |
15 | 14 | rspcev 2843 |
. . . . . . . 8
                

        |
16 | 1, 4, 11, 15 | syl12anc 1236 |
. . . . . . 7
    TopOn 
TopOn                   

        |
17 | 16 | expr 375 |
. . . . . 6
    TopOn 
TopOn                  

         |
18 | 17 | ralrimiva 2550 |
. . . . 5
   TopOn  TopOn 

  
     

    


         |
19 | 18 | expr 375 |
. . . 4
   TopOn  TopOn 

 
             
          |
20 | 19 | pm4.71d 393 |
. . 3
   TopOn  TopOn 

 
                


           |
21 | | simpl2 1001 |
. . . . 5
   TopOn  TopOn 

 
 TopOn    |
22 | | toponmax 13564 |
. . . . 5
 TopOn 
  |
23 | 21, 22 | syl 14 |
. . . 4
   TopOn  TopOn 

 
   |
24 | | simpl1 1000 |
. . . . 5
   TopOn  TopOn 

 
 TopOn    |
25 | | toponmax 13564 |
. . . . 5
 TopOn 
  |
26 | 24, 25 | syl 14 |
. . . 4
   TopOn  TopOn 

 
   |
27 | 23, 26 | elmapd 6664 |
. . 3
   TopOn  TopOn 

 
           |
28 | | iscnp3 13742 |
. . . 4
  TopOn  TopOn 

                 


           |
29 | 28 | adantr 276 |
. . 3
   TopOn  TopOn 

 
                   

           |
30 | 20, 27, 29 | 3bitr4rd 221 |
. 2
   TopOn  TopOn 

 
             |
31 | 30 | eqrdv 2175 |
1
   TopOn  TopOn 

 
           |