Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . . 10
           |
2 | 1 | feqmptd 5945 |
. . . . . . . . 9
             |
3 | 2 | cnveqd 5032 |
. . . . . . . 8
               |
4 | 3 | imaeq1d 5189 |
. . . . . . 7
                       |
5 | 4 | ad2antrr 737 |
. . . . . 6
                           |
6 | | exmid 421 |
. . . . . . . . . . 11
        ↾t 
       
       ↾t    
       |
7 | 6 | biantrur 513 |
. . . . . . . . . 10
    
 
       ↾t    
           
↾t    
     
       |
8 | | andir 884 |
. . . . . . . . . 10
         
↾t    
           
↾t    
     
              ↾t 
             
      
↾t    
             |
9 | 7, 8 | bitri 257 |
. . . . . . . . 9
    
 
       ↾t    
                  ↾t 
                |
10 | | retopbas 21836 |
. . . . . . . . . . . . . . . . . 18
 |
11 | | bastg 20036 |
. . . . . . . . . . . . . . . . . 18

      |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
     |
13 | 12 | sseli 3440 |
. . . . . . . . . . . . . . . 16
       |
14 | 13 | ad2antlr 738 |
. . . . . . . . . . . . . . 15
         
       |
15 | | cnpimaex 20327 |
. . . . . . . . . . . . . . . . 17
         ↾t    
    
  
            ↾t           |
16 | 15 | 3com12 1219 |
. . . . . . . . . . . . . . . 16
             ↾t 
                   ↾t           |
17 | 16 | 3expa 1215 |
. . . . . . . . . . . . . . 15
      
      
↾t    
     
    
      ↾t           |
18 | 14, 17 | sylanl1 660 |
. . . . . . . . . . . . . 14
         

         ↾t 
              
     ↾t           |
19 | 18 | ex 440 |
. . . . . . . . . . . . 13
        

         ↾t 
                    ↾t            |
20 | | simprrr 780 |
. . . . . . . . . . . . . . . 16
             
↾t         
      |
21 | | ffn 5755 |
. . . . . . . . . . . . . . . . . . 19
       |
22 | 21 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
     
   |
23 | | restsspw 15385 |
. . . . . . . . . . . . . . . . . . . 20
     ↾t 
  |
24 | 23 | sseli 3440 |
. . . . . . . . . . . . . . . . . . 19
     
↾t     |
25 | 24 | elpwid 3973 |
. . . . . . . . . . . . . . . . . 18
     
↾t    |
26 | | simpl 463 |
. . . . . . . . . . . . . . . . . 18
      
  |
27 | | fnfvima 6173 |
. . . . . . . . . . . . . . . . . 18
             |
28 | 22, 25, 26, 27 | syl3an 1318 |
. . . . . . . . . . . . . . . . 17
             ↾t                   |
29 | 28 | 3expb 1216 |
. . . . . . . . . . . . . . . 16
             
↾t         
          |
30 | 20, 29 | sseldd 3445 |
. . . . . . . . . . . . . . 15
             
↾t         
      |
31 | 30 | rexlimdvaa 2892 |
. . . . . . . . . . . . . 14
     
        ↾t                |
32 | 31 | ad3antrrr 741 |
. . . . . . . . . . . . 13
        

         ↾t 
                ↾t                |
33 | 19, 32 | impbid 195 |
. . . . . . . . . . . 12
        

         ↾t 
              
     ↾t            |
34 | 33 | pm5.32da 651 |
. . . . . . . . . . 11
         
          ↾t 
            
        ↾t 
        
   
 ↾t             |
35 | | r19.42v 2957 |
. . . . . . . . . . 11
       ↾t           ↾t 
                      
↾t    
           ↾t            |
36 | 34, 35 | syl6bbr 271 |
. . . . . . . . . 10
         
          ↾t 
            
      ↾t           ↾t 
                  |
37 | 36 | orbi1d 714 |
. . . . . . . . 9
         
           ↾t 
             
      
↾t    
                  ↾t           ↾t 
                       ↾t 
                 |
38 | 9, 37 | syl5bb 265 |
. . . . . . . 8
         
             ↾t           ↾t 
                       ↾t 
                 |
39 | 38 | rabbidva 3047 |
. . . . . . 7
         
             ↾t           ↾t 
                       ↾t 
                 |
40 | | eqid 2462 |
. . . . . . . 8
             |
41 | 40 | mptpreima 5351 |
. . . . . . 7
           
      |
42 | | unrab 3726 |
. . . . . . 7
  
     ↾t           ↾t 
                

      
↾t    
                    ↾t           ↾t 
                       ↾t 
                |
43 | 39, 41, 42 | 3eqtr4g 2521 |
. . . . . 6
                            ↾t           ↾t 
                

      
↾t    
              |
44 | 5, 43 | eqtrd 2496 |
. . . . 5
               

   
 ↾t           ↾t 
                

      
↾t    
              |
45 | 44 | 3adantl3 1172 |
. . . 4
                     ↾t 
            
              ↾t           ↾t 
                

      
↾t    
              |
46 | | incom 3637 |
. . . . . . . . 9
 
   
 ↾t           
       ↾t    
        
      
↾t    
            ↾t             |
47 | | dfin4 3695 |
. . . . . . . . 9
 
   
 ↾t           
       ↾t    
              ↾t                  ↾t           
      
↾t    
         |
48 | | inrab 3727 |
. . . . . . . . . . . 12
 
       ↾t    
                        ↾t 
                 |
49 | 48 | a1i 11 |
. . . . . . . . . . 11
     
↾t   
      
↾t    
                        ↾t 
                  |
50 | 49 | iuneq2i 4311 |
. . . . . . . . . 10
      ↾t    
       ↾t    
                     ↾t   

       ↾t    
              |
51 | | iunin2 4356 |
. . . . . . . . . 10
      ↾t    
       ↾t    
                
       ↾t 
               ↾t             |
52 | | iunrab 4339 |
. . . . . . . . . 10
      ↾t   

       ↾t    
             
      ↾t           ↾t 
                 |
53 | 50, 51, 52 | 3eqtr3i 2492 |
. . . . . . . . 9
 
       ↾t    
            ↾t                   ↾t           ↾t 
                 |
54 | 46, 47, 53 | 3eqtr3i 2492 |
. . . . . . . 8
 
   
 ↾t                  ↾t           
      
↾t    
               ↾t           ↾t 
                 |
55 | | eqeq2 2473 |
. . . . . . . . . . . . 13
           
                           |
56 | | eqeq2 2473 |
. . . . . . . . . . . . 13
       
 
                             |
57 | | simprrl 779 |
. . . . . . . . . . . . . . . 16
        ↾t 
    

       
  |
58 | 25 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
       ↾t 
    
  |
59 | 58 | sselda 3444 |
. . . . . . . . . . . . . . . . 17
        ↾t 
    
   |
60 | | pm3.22 455 |
. . . . . . . . . . . . . . . . . 18
     
         |
61 | 60 | adantll 725 |
. . . . . . . . . . . . . . . . 17
        ↾t 
    
         |
62 | 59, 61 | jca 539 |
. . . . . . . . . . . . . . . 16
        ↾t 
    
  
   
    |
63 | 57, 62 | impbida 848 |
. . . . . . . . . . . . . . 15
       ↾t 
    
  
   
 
   |
64 | 63 | abbidv 2580 |
. . . . . . . . . . . . . 14
       ↾t 
    
              |
65 | | df-rab 2758 |
. . . . . . . . . . . . . 14

                  |
66 | | cvjust 2457 |
. . . . . . . . . . . . . 14
   |
67 | 64, 65, 66 | 3eqtr4g 2521 |
. . . . . . . . . . . . 13
       ↾t 
    

         |
68 | | simpr 467 |
. . . . . . . . . . . . . . . . 17
          
  |
69 | 68 | con3i 142 |
. . . . . . . . . . . . . . . 16
    
        |
70 | 69 | ralrimivw 2815 |
. . . . . . . . . . . . . . 15
    
 
   
   |
71 | | rabeq0 3766 |
. . . . . . . . . . . . . . 15
         

   
   |
72 | 70, 71 | sylibr 217 |
. . . . . . . . . . . . . 14
    
          |
73 | 72 | adantl 472 |
. . . . . . . . . . . . 13
       ↾t 
     
         |
74 | 55, 56, 67, 73 | ifbothda 3928 |
. . . . . . . . . . . 12
     
↾t  
                  |
75 | 74 | iuneq2i 4311 |
. . . . . . . . . . 11
      ↾t   
             ↾t        
    |
76 | | retop 21837 |
. . . . . . . . . . . . . 14
     |
77 | | resttop 20231 |
. . . . . . . . . . . . . 14
            ↾t    |
78 | 76, 77 | mpan 681 |
. . . . . . . . . . . . 13
      ↾t    |
79 | | 0opn 19989 |
. . . . . . . . . . . . . . . 16
      ↾t       ↾t    |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . 15
      ↾t    |
81 | | ifcl 3935 |
. . . . . . . . . . . . . . . 16
       ↾t 
     ↾t           
   
 ↾t    |
82 | 81 | ancoms 459 |
. . . . . . . . . . . . . . 15
 
   
 ↾t 
     ↾t           
   
 ↾t    |
83 | 80, 82 | sylan 478 |
. . . . . . . . . . . . . 14
       ↾t           
   
 ↾t    |
84 | 83 | ralrimiva 2814 |
. . . . . . . . . . . . 13
       ↾t                 ↾t    |
85 | | iunopn 19983 |
. . . . . . . . . . . . 13
       ↾t        ↾t                 ↾t         ↾t        
        ↾t    |
86 | 78, 84, 85 | syl2anc 671 |
. . . . . . . . . . . 12
       ↾t                 ↾t    |
87 | | eqid 2462 |
. . . . . . . . . . . . 13
     ↾t       ↾t   |
88 | 87 | subopnmbl 22618 |
. . . . . . . . . . . 12
        ↾t                 ↾t         ↾t        
     |
89 | 86, 88 | mpdan 679 |
. . . . . . . . . . 11
       ↾t              |
90 | 75, 89 | syl5eqel 2544 |
. . . . . . . . . 10
       ↾t             |
91 | 90 | adantr 471 |
. . . . . . . . 9
      
         ↾t 
             
     ↾t             |
92 | | difss 3572 |
. . . . . . . . . . . . 13
 
   
 ↾t           
      
↾t    
             ↾t   
        |
93 | | ssrab2 3526 |
. . . . . . . . . . . . . . 15

        |
94 | 93 | rgenw 2761 |
. . . . . . . . . . . . . 14
      ↾t   
        |
95 | | iunss 4333 |
. . . . . . . . . . . . . 14
 
   
 ↾t                 ↾t             |
96 | 94, 95 | mpbir 214 |
. . . . . . . . . . . . 13
      ↾t   
        |
97 | 92, 96 | sstri 3453 |
. . . . . . . . . . . 12
 
   
 ↾t           
      
↾t    
        |
98 | | mblss 22540 |
. . . . . . . . . . . 12
   |
99 | 97, 98 | syl5ss 3455 |
. . . . . . . . . . 11
        ↾t           
      
↾t    
         |
100 | 99 | adantr 471 |
. . . . . . . . . 10
      
         ↾t 
                    ↾t           
      
↾t    
         |
101 | | ssdif 3580 |
. . . . . . . . . . . . . 14
 
   
 ↾t                  ↾t   
               ↾t 
           
      
↾t    
         |
102 | 96, 101 | ax-mp 5 |
. . . . . . . . . . . . 13
 
   
 ↾t           
      
↾t    
                ↾t 
           |
103 | | ovex 6348 |
. . . . . . . . . . . . . . . . . . . . 21
   |
104 | 103 | rabex 4571 |
. . . . . . . . . . . . . . . . . . . 20
   
                ↾t            |
105 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . . 20
    
                ↾t                                 ↾t             |
106 | 104, 105 | fnmpti 5732 |
. . . . . . . . . . . . . . . . . . 19
    
                ↾t             |
107 | | retopon 21839 |
. . . . . . . . . . . . . . . . . . . . . 22
    TopOn   |
108 | | resttopon 20232 |
. . . . . . . . . . . . . . . . . . . . . 22
      TopOn 
     
↾t  TopOn    |
109 | 107, 98, 108 | sylancr 674 |
. . . . . . . . . . . . . . . . . . . . 21
      ↾t  TopOn    |
110 | | cnpfval 20305 |
. . . . . . . . . . . . . . . . . . . . 21
       ↾t  TopOn    
 TopOn  
      ↾t 
                          ↾t              |
111 | 109, 107,
110 | sylancl 673 |
. . . . . . . . . . . . . . . . . . . 20
       ↾t    
      
                ↾t              |
112 | 111 | fneq1d 5692 |
. . . . . . . . . . . . . . . . . . 19
       
↾t    
 

   
                ↾t               |
113 | 106, 112 | mpbiri 241 |
. . . . . . . . . . . . . . . . . 18
       ↾t    
    |
114 | | elpreima 6030 |
. . . . . . . . . . . . . . . . . 18
       ↾t    
           ↾t 
           

      
↾t    
    
        |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . 17
         
↾t    
                 ↾t    
    
        |
116 | | rele 4985 |
. . . . . . . . . . . . . . . . . . . 20
 |
117 | | elrelimasn 5214 |
. . . . . . . . . . . . . . . . . . . 20
         ↾t    
    
   
       ↾t 
           |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
       
↾t    
    
   
       ↾t 
          |
119 | | fvex 5902 |
. . . . . . . . . . . . . . . . . . . 20
       ↾t    
      |
120 | 119 | epelc 4769 |
. . . . . . . . . . . . . . . . . . 19
        ↾t 
       
       ↾t 
          |
121 | 118, 120 | bitr2i 258 |
. . . . . . . . . . . . . . . . . 18
        ↾t 
       
       ↾t    
    
      |
122 | 121 | anbi2i 705 |
. . . . . . . . . . . . . . . . 17
 
       ↾t    
              ↾t    
    
       |
123 | 115, 122 | syl6rbbr 272 |
. . . . . . . . . . . . . . . 16
  
      
↾t    
     
        ↾t 
               |
124 | 123 | abbidv 2580 |
. . . . . . . . . . . . . . 15
          ↾t 
                  
↾t    
            |
125 | | df-rab 2758 |
. . . . . . . . . . . . . . 15

       ↾t 
         

       ↾t    
        |
126 | | imaco 5363 |
. . . . . . . . . . . . . . . 16
         ↾t 
                  ↾t 
             |
127 | | abid2 2584 |
. . . . . . . . . . . . . . . 16

        ↾t 
                     ↾t    
          |
128 | 126, 127 | eqtr4i 2487 |
. . . . . . . . . . . . . . 15
         ↾t 
                   ↾t 
              |
129 | 124, 125,
128 | 3eqtr4g 2521 |
. . . . . . . . . . . . . 14
 
       ↾t    
     
         ↾t 
            |
130 | 129 | difeq2d 3563 |
. . . . . . . . . . . . 13
  
       ↾t 
                    ↾t    
          |
131 | 102, 130 | syl5sseq 3492 |
. . . . . . . . . . . 12
        ↾t           
      
↾t    
                
↾t    
          |
132 | | difss 3572 |
. . . . . . . . . . . . 13
         
↾t    
       
 |
133 | 132, 98 | syl5ss 3455 |
. . . . . . . . . . . 12
           ↾t 
             |
134 | 131, 133 | jca 539 |
. . . . . . . . . . 11
         ↾t   
               ↾t 
                    ↾t    
                 
↾t    
       
   |
135 | | ovolssnul 22495 |
. . . . . . . . . . . 12
         ↾t   
               ↾t 
                    ↾t    
                 
↾t    
       
             
↾t    
         
           ↾t   
               ↾t 
             |
136 | 135 | 3expa 1215 |
. . . . . . . . . . 11
          ↾t   
               ↾t 
                    ↾t    
                 
↾t    
       
     
         ↾t 
                        ↾t           
      
↾t    
          |
137 | 134, 136 | sylan 478 |
. . . . . . . . . 10
      
         ↾t 
                        ↾t           
      
↾t    
          |
138 | | nulmbl 22544 |
. . . . . . . . . 10
         ↾t   
               ↾t 
         
     
   
 ↾t           
      
↾t    
          
     ↾t           
      
↾t    
         |
139 | 100, 137,
138 | syl2anc 671 |
. . . . . . . . 9
      
         ↾t 
                    ↾t           
      
↾t    
         |
140 | | difmbl 22552 |
. . . . . . . . 9
        ↾t            
   
 ↾t           
      
↾t    
       
 
   
 ↾t                  ↾t           
      
↾t    
          |
141 | 91, 139, 140 | syl2anc 671 |
. . . . . . . 8
      
         ↾t 
                    ↾t                  ↾t           
      
↾t    
          |
142 | 54, 141 | syl5eqelr 2545 |
. . . . . . 7
      
         ↾t 
             
      ↾t           ↾t 
                  |
143 | | ssrab2 3526 |
. . . . . . . . . 10


      
↾t    
          
 |
144 | 143, 98 | syl5ss 3455 |
. . . . . . . . 9
          ↾t 
                |
145 | 144 | adantr 471 |
. . . . . . . 8
      
         ↾t 
             
        ↾t 
                |
146 | 126 | eleq2i 2532 |
. . . . . . . . . . . . . . . 16
         
↾t    
              
↾t    
           |
147 | | ibar 511 |
. . . . . . . . . . . . . . . . . 18
         ↾t 
           

      
↾t    
    
        |
148 | 121, 147 | syl5rbb 266 |
. . . . . . . . . . . . . . . . 17
          ↾t 
            
       ↾t 
           |
149 | 115, 148 | sylan9bb 711 |
. . . . . . . . . . . . . . . 16
            ↾t 
           
       ↾t 
           |
150 | 146, 149 | syl5rbb 266 |
. . . . . . . . . . . . . . 15
           ↾t 
       
         ↾t    
          |
151 | 150 | notbid 300 |
. . . . . . . . . . . . . 14
           ↾t 
       
         ↾t    
          |
152 | 151 | biimpd 212 |
. . . . . . . . . . . . 13
           ↾t 
       
         ↾t 
             |
153 | 152 | adantrd 474 |
. . . . . . . . . . . 12
            ↾t    
         
         ↾t    
          |
154 | 153 | ss2rabdv 3522 |
. . . . . . . . . . 11
          ↾t 
              
         ↾t 
             |
155 | | dfdif2 3425 |
. . . . . . . . . . 11
         
↾t    
        
         ↾t 
            |
156 | 154, 155 | syl6sseqr 3491 |
. . . . . . . . . 10
          ↾t 
              
         ↾t 
             |
157 | 156, 133 | jca 539 |
. . . . . . . . 9
           ↾t 
              
         ↾t 
           
         ↾t 
              |
158 | | ovolssnul 22495 |
. . . . . . . . . 10
           ↾t 
              
         ↾t 
           
         ↾t 
                         ↾t 
                 
        ↾t 
                 |
159 | 158 | 3expa 1215 |
. . . . . . . . 9
            ↾t    
          
          ↾t    
                 
↾t    
       
     
         ↾t 
                 
        ↾t 
                 |
160 | 157, 159 | sylan 478 |
. . . . . . . 8
      
         ↾t 
                 
        ↾t 
                 |
161 | | nulmbl 22544 |
. . . . . . . 8
           ↾t 
                           ↾t 
                
        ↾t 
                |
162 | 145, 160,
161 | syl2anc 671 |
. . . . . . 7
      
         ↾t 
             
        ↾t 
                |
163 | | unmbl 22546 |
. . . . . . 7
         ↾t           ↾t 
                         ↾t 
                
      ↾t           ↾t 
                

      
↾t    
              |
164 | 142, 162,
163 | syl2anc 671 |
. . . . . 6
      
         ↾t 
                     ↾t           ↾t 
                

      
↾t    
              |
165 | 164 | 3adant1 1032 |
. . . . 5
     
             
↾t    
         
  
     ↾t           ↾t 
                

      
↾t    
              |
166 | 165 | adantr 471 |
. . . 4
                     ↾t 
            
         ↾t           ↾t 
                

      
↾t    
              |
167 | 45, 166 | eqeltrd 2540 |
. . 3
                     ↾t 
            
        |
168 | 167 | ralrimiva 2814 |
. 2
     
             
↾t    
         
         |
169 | | ismbf 22642 |
. . 3
      MblFn
          |
170 | 169 | 3ad2ant1 1035 |
. 2
     
             
↾t    
         
 MblFn 
         |
171 | 168, 170 | mpbird 240 |
1
     
             
↾t    
         
MblFn |