Step | Hyp | Ref
| Expression |
1 | | distop 20088 |
. . . . 5
 
  |
2 | 1 | adantl 473 |
. . . 4
 
    |
3 | | simpl 464 |
. . . 4
 
   |
4 | | unipw 4650 |
. . . . . 6
 
 |
5 | 4 | eqcomi 2480 |
. . . . 5
   |
6 | | eqid 2471 |
. . . . 5
   
↾t      
↾t    |
7 | | eqid 2471 |
. . . . 5
    
↾t                  
↾t               |
8 | 5, 6, 7 | xkoval 20679 |
. . . 4
                 
  ↾t                  |
9 | 2, 3, 8 | syl2anc 673 |
. . 3
 
              
  ↾t                  |
10 | | simpr 468 |
. . . . 5
 
   |
11 | | fconst6g 5785 |
. . . . . 6
           |
12 | 11 | adantr 472 |
. . . . 5
 
           |
13 | | pttop 20674 |
. . . . 5
  
       
          |
14 | 10, 12, 13 | syl2anc 673 |
. . . 4
 
           |
15 | | elpwi 3951 |
. . . . . . . . . . . . . 14
    |
16 | | restdis 20271 |
. . . . . . . . . . . . . 14
     ↾t     |
17 | 15, 16 | sylan2 482 |
. . . . . . . . . . . . 13
 
 
  ↾t     |
18 | 17 | adantll 728 |
. . . . . . . . . . . 12
       
↾t     |
19 | 18 | eleq1d 2533 |
. . . . . . . . . . 11
         ↾t 
    |
20 | | discmp 20490 |
. . . . . . . . . . 11

   |
21 | 19, 20 | syl6bbr 271 |
. . . . . . . . . 10
         ↾t 
   |
22 | 21 | rabbidva 3021 |
. . . . . . . . 9
 
  
  ↾t        |
23 | | dfin5 3398 |
. . . . . . . . 9
    
  |
24 | 22, 23 | syl6eqr 2523 |
. . . . . . . 8
 
  
  ↾t        |
25 | | eqidd 2472 |
. . . . . . . 8
 
   |
26 | | eqid 2471 |
. . . . . . . . . . 11
   |
27 | 26 | toptopon 20025 |
. . . . . . . . . 10

TopOn     |
28 | | cndis 20384 |
. . . . . . . . . . 11
 
TopOn            |
29 | 28 | ancoms 460 |
. . . . . . . . . 10
  TopOn     
      |
30 | 27, 29 | sylanb 480 |
. . . . . . . . 9
 
         |
31 | | rabeq 3024 |
. . . . . . . . 9
               
       
   |
32 | 30, 31 | syl 17 |
. . . . . . . 8
 
         
       
   |
33 | 24, 25, 32 | mpt2eq123dv 6372 |
. . . . . . 7
 
      ↾t                  
            |
34 | 33 | rneqd 5068 |
. . . . . 6
 
   
  ↾t                  
            |
35 | | eqid 2471 |
. . . . . . 7
                               |
36 | 35 | rnmpt2 6425 |
. . . . . 6
    
                        
   |
37 | 34, 36 | syl6eq 2521 |
. . . . 5
 
   
  ↾t                            
    |
38 | | elmapi 7511 |
. . . . . . . . . . . 12
           |
39 | | eleq2 2538 |
. . . . . . . . . . . . . . . . 17
                 
       |
40 | 39 | imbi2d 323 |
. . . . . . . . . . . . . . . 16
             

              |
41 | 40 | bibi1d 326 |
. . . . . . . . . . . . . . 15
                     
            

         |
42 | | eleq2 2538 |
. . . . . . . . . . . . . . . . 17
 
     
     
     
       |
43 | 42 | imbi2d 323 |
. . . . . . . . . . . . . . . 16
 
     
        
     
        |
44 | 43 | bibi1d 326 |
. . . . . . . . . . . . . . 15
 
     
         
     
            

         |
45 | | inss1 3643 |
. . . . . . . . . . . . . . . . . . . . 21
     |
46 | | simprl 772 |
. . . . . . . . . . . . . . . . . . . . 21
               |
47 | 45, 46 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . 20
             |
48 | 47 | elpwid 3952 |
. . . . . . . . . . . . . . . . . . 19
         
  |
49 | 48 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
   
    
       
  |
50 | 49 | sselda 3418 |
. . . . . . . . . . . . . . . . 17
         
       
   |
51 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
         
       
   |
52 | 50, 51 | 2thd 248 |
. . . . . . . . . . . . . . . 16
         
       
     |
53 | 52 | imbi1d 324 |
. . . . . . . . . . . . . . 15
         
       
  
     
        |
54 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . . 19
      

       |
55 | 54 | ex 441 |
. . . . . . . . . . . . . . . . . 18
               |
56 | 55 | adantl 473 |
. . . . . . . . . . . . . . . . 17
   
    
                 |
57 | 56 | adantr 472 |
. . . . . . . . . . . . . . . 16
         
       


        |
58 | | pm2.21 111 |
. . . . . . . . . . . . . . . . 17
         |
59 | 58 | adantl 473 |
. . . . . . . . . . . . . . . 16
         
       


       |
60 | 57, 59 | 2thd 248 |
. . . . . . . . . . . . . . 15
         
       

        
        |
61 | 41, 44, 53, 60 | ifbothda 3907 |
. . . . . . . . . . . . . 14
   
    
         
     
    

        |
62 | 61 | ralbidv2 2827 |
. . . . . . . . . . . . 13
   
    
               
   

       |
63 | | ffn 5739 |
. . . . . . . . . . . . . . 15
        |
64 | 63 | adantl 473 |
. . . . . . . . . . . . . 14
   
    
          |
65 | | vex 3034 |
. . . . . . . . . . . . . . . 16
 |
66 | 65 | elixp 7547 |
. . . . . . . . . . . . . . 15
       


     
       |
67 | 66 | baib 919 |
. . . . . . . . . . . . . 14
  
                    |
68 | 64, 67 | syl 17 |
. . . . . . . . . . . . 13
   
    
         
 
   

     
       |
69 | | ffun 5742 |
. . . . . . . . . . . . . . 15
        |
70 | 69 | adantl 473 |
. . . . . . . . . . . . . 14
   
    
          |
71 | | fdm 5745 |
. . . . . . . . . . . . . . . 16
        |
72 | 71 | adantl 473 |
. . . . . . . . . . . . . . 15
   
    
       
  |
73 | 49, 72 | sseqtr4d 3455 |
. . . . . . . . . . . . . 14
   
    
       
  |
74 | | funimass4 5930 |
. . . . . . . . . . . . . 14
                |
75 | 70, 73, 74 | syl2anc 673 |
. . . . . . . . . . . . 13
   
    
                     |
76 | 62, 68, 75 | 3bitr4d 293 |
. . . . . . . . . . . 12
   
    
         
 
   
       |
77 | 38, 76 | sylan2 482 |
. . . . . . . . . . 11
   
    
       
 
   
       |
78 | 77 | rabbi2dva 3631 |
. . . . . . . . . 10
              
              
   |
79 | | elssuni 4219 |
. . . . . . . . . . . . . . . 16
    |
80 | 79 | ad2antll 743 |
. . . . . . . . . . . . . . 15
         
   |
81 | | ssid 3437 |
. . . . . . . . . . . . . . 15
   |
82 | | sseq1 3439 |
. . . . . . . . . . . . . . . 16
                   |
83 | | sseq1 3439 |
. . . . . . . . . . . . . . . 16
 
     
  
     
    |
84 | 82, 83 | ifboth 3908 |
. . . . . . . . . . . . . . 15
 
 
           |
85 | 80, 81, 84 | sylancl 675 |
. . . . . . . . . . . . . 14
                   |
86 | 85 | ralrimivw 2810 |
. . . . . . . . . . . . 13
          
         |
87 | | ss2ixp 7553 |
. . . . . . . . . . . . 13
 
 
            
   |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . 12
            
    
   |
89 | | simplr 770 |
. . . . . . . . . . . . 13
         
  |
90 | | uniexg 6607 |
. . . . . . . . . . . . . 14
    |
91 | 90 | ad2antrr 740 |
. . . . . . . . . . . . 13
          
  |
92 | | ixpconstg 7549 |
. . . . . . . . . . . . 13
     
 
   |
93 | 89, 91, 92 | syl2anc 673 |
. . . . . . . . . . . 12
           
     |
94 | 88, 93 | sseqtrd 3454 |
. . . . . . . . . . 11
            
     
   |
95 | | dfss1 3628 |
. . . . . . . . . . 11
 
 
     
     
       
 
      |
96 | 94, 95 | sylib 201 |
. . . . . . . . . 10
              
       
 
      |
97 | 78, 96 | eqtr3d 2507 |
. . . . . . . . 9
                  

        |
98 | 11 | ad2antrr 740 |
. . . . . . . . . 10
                    |
99 | | inss2 3644 |
. . . . . . . . . . 11
    |
100 | 99, 46 | sseldi 3416 |
. . . . . . . . . 10
            |
101 | | simplrr 779 |
. . . . . . . . . . . 12
   
    
     |
102 | 26 | topopn 20013 |
. . . . . . . . . . . . 13
    |
103 | 102 | ad3antrrr 744 |
. . . . . . . . . . . 12
   
    
      |
104 | 101, 103 | ifcld 3915 |
. . . . . . . . . . 11
   
    
    
      |
105 | | simpll 768 |
. . . . . . . . . . . 12
         
  |
106 | | fvconst2g 6134 |
. . . . . . . . . . . 12
 
           |
107 | 105, 106 | sylan 479 |
. . . . . . . . . . 11
   
    
             |
108 | 104, 107 | eleqtrrd 2552 |
. . . . . . . . . 10
   
    
    
              |
109 | | eldifn 3545 |
. . . . . . . . . . . . 13
  
  |
110 | 109 | iffalsed 3883 |
. . . . . . . . . . . 12
    
       |
111 | 110 | adantl 473 |
. . . . . . . . . . 11
   
    
      
       |
112 | | eldifi 3544 |
. . . . . . . . . . . . 13
     |
113 | 112, 107 | sylan2 482 |
. . . . . . . . . . . 12
   
    
               |
114 | 113 | unieqd 4200 |
. . . . . . . . . . 11
   
    
                 |
115 | 111, 114 | eqtr4d 2508 |
. . . . . . . . . 10
   
    
      
               |
116 | 89, 98, 100, 108, 115 | ptopn 20675 |
. . . . . . . . 9
            
              |
117 | 97, 116 | eqeltrd 2549 |
. . . . . . . 8
                  
          |
118 | | eleq1 2537 |
. . . . . . . 8
                  
                    |
119 | 117, 118 | syl5ibrcom 230 |
. . . . . . 7
                  
            |
120 | 119 | rexlimdvva 2878 |
. . . . . 6
 
               
            |
121 | 120 | abssdv 3489 |
. . . . 5
 
  
                         |
122 | 37, 121 | eqsstrd 3452 |
. . . 4
 
   
  ↾t                        |
123 | | tgfiss 20084 |
. . . 4
            
  ↾t                      
           ↾t                          |
124 | 14, 122, 123 | syl2anc 673 |
. . 3
 
         
  ↾t                          |
125 | 9, 124 | eqsstrd 3452 |
. 2
 
                |
126 | | eqid 2471 |
. . . . . . . 8
                 |
127 | 126, 26 | ptuniconst 20690 |
. . . . . . 7
 
               |
128 | 127 | ancoms 460 |
. . . . . 6
 
               |
129 | 30, 128 | eqtrd 2505 |
. . . . 5
 
               |
130 | 129 | oveq2d 6324 |
. . . 4
 
         
↾t             
↾t             |
131 | | eqid 2471 |
. . . . . 6
                   |
132 | 131 | restid 15410 |
. . . . 5
                 
↾t                     |
133 | 14, 132 | syl 17 |
. . . 4
 
         
↾t                     |
134 | 130, 133 | eqtrd 2505 |
. . 3
 
         
↾t               |
135 | 5, 126 | xkoptsub 20746 |
. . . 4
            
↾t     
      |
136 | 2, 3, 135 | syl2anc 673 |
. . 3
 
         
↾t     
      |
137 | 134, 136 | eqsstr3d 3453 |
. 2
 
                |
138 | 125, 137 | eqssd 3435 |
1
 
                |