Step | Hyp | Ref
| Expression |
1 | | simpll 768 |
. . . . 5
               CnExt         
  |
2 | | simpll 768 |
. . . . . . . . 9
                CnExt                                     |
3 | | simpr3 1038 |
. . . . . . . . 9
                CnExt                                                   |
4 | | cnextf.3 |
. . . . . . . . . . 11
   |
5 | 4 | ad2antrr 740 |
. . . . . . . . . 10
                CnExt                                  
  |
6 | | simpr2 1037 |
. . . . . . . . . 10
                CnExt                                               |
7 | | neii2 20201 |
. . . . . . . . . 10
 
          

  
   |
8 | 5, 6, 7 | syl2anc 673 |
. . . . . . . . 9
                CnExt                                   
      |
9 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . 20
 |
10 | 9 | snss 4087 |
. . . . . . . . . . . . . . . . . . 19

    |
11 | 10 | biimpri 211 |
. . . . . . . . . . . . . . . . . 18
     |
12 | 11 | anim1i 578 |
. . . . . . . . . . . . . . . . 17
    

   |
13 | 12 | anim2i 579 |
. . . . . . . . . . . . . . . 16
        
    |
14 | 13 | anim2i 579 |
. . . . . . . . . . . . . . 15
 

      
 
     |
15 | 14 | ex 441 |
. . . . . . . . . . . . . 14
     
 
         |
16 | | 3anass 1011 |
. . . . . . . . . . . . . . . . 17
 
  
    |
17 | 16 | anbi1i 709 |
. . . . . . . . . . . . . . . 16
  
 
        |
18 | | anass 661 |
. . . . . . . . . . . . . . . 16
   
 

        |
19 | | anass 661 |
. . . . . . . . . . . . . . . . 17
  



     |
20 | 19 | anbi2i 708 |
. . . . . . . . . . . . . . . 16
 
 

          |
21 | 17, 18, 20 | 3bitri 279 |
. . . . . . . . . . . . . . 15
  
 
        |
22 | | opnneip 20212 |
. . . . . . . . . . . . . . . . . 18
 
             |
23 | 4, 22 | syl3an1 1325 |
. . . . . . . . . . . . . . . . 17
 

            |
24 | 23 | adantr 472 |
. . . . . . . . . . . . . . . 16
  
              |
25 | | simpr2 1037 |
. . . . . . . . . . . . . . . . . 18
 
     |
26 | 25 | ex 441 |
. . . . . . . . . . . . . . . . 17
  
    |
27 | 26 | imdistanri 705 |
. . . . . . . . . . . . . . . 16
  
      |
28 | 24, 27 | jca 541 |
. . . . . . . . . . . . . . 15
  
            

    |
29 | 21, 28 | sylbir 218 |
. . . . . . . . . . . . . 14
 

   
                |
30 | 15, 29 | syl6 33 |
. . . . . . . . . . . . 13
     
 
                 |
31 | 30 | adantr 472 |
. . . . . . . . . . . 12
 
             
     
 
                 |
32 | | cnextf.4 |
. . . . . . . . . . . . . . . . . . . 20
   |
33 | | haustop 20424 |
. . . . . . . . . . . . . . . . . . . 20

  |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
   |
35 | 34 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
   |
36 | | imassrn 5185 |
. . . . . . . . . . . . . . . . . . . 20
       |
37 | | cnextf.5 |
. . . . . . . . . . . . . . . . . . . . 21
       |
38 | | frn 5747 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   |
40 | 36, 39 | syl5ss 3429 |
. . . . . . . . . . . . . . . . . . 19
    
 
  |
41 | 40 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
         |
42 | | ssrin 3648 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
43 | | imass2 5210 |
. . . . . . . . . . . . . . . . . . . 20
                   |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
               |
45 | 44 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
 
               |
46 | | cnextf.2 |
. . . . . . . . . . . . . . . . . . 19
  |
47 | 46 | clsss 20146 |
. . . . . . . . . . . . . . . . . 18
                    
             
                |
48 | 35, 41, 45, 47 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
 
                               |
49 | | sstr 3426 |
. . . . . . . . . . . . . . . . 17
                                                             |
50 | 48, 49 | sylan 479 |
. . . . . . . . . . . . . . . 16
                                   |
51 | 50 | an32s 821 |
. . . . . . . . . . . . . . 15
                                   |
52 | 51 | ex 441 |
. . . . . . . . . . . . . 14
 
             
                   |
53 | 52 | anim2d 575 |
. . . . . . . . . . . . 13
 
             
                       |
54 | 53 | anim2d 575 |
. . . . . . . . . . . 12
 
             
                                               |
55 | 31, 54 | syld 44 |
. . . . . . . . . . 11
 
             
     
 
                               |
56 | 55 | reximdv2 2855 |
. . . . . . . . . 10
 
             
                                      |
57 | 56 | imp 436 |
. . . . . . . . 9
                  
                                   |
58 | 2, 3, 8, 57 | syl21anc 1291 |
. . . . . . . 8
                CnExt                                   
                             |
59 | 58 | 3anassrs 1256 |
. . . . . . 7
                 CnExt                                                                  |
60 | | simpr 468 |
. . . . . . . . 9
                 CnExt                     ↾t                              |
61 | | simp-4l 784 |
. . . . . . . . 9
                 CnExt                     ↾t                  |
62 | | simplr 770 |
. . . . . . . . 9
                 CnExt                     ↾t                           ↾t    |
63 | | fvex 5889 |
. . . . . . . . . . . . . 14
           |
64 | 63 | a1i 11 |
. . . . . . . . . . . . 13
             |
65 | | cnextf.1 |
. . . . . . . . . . . . . . . . 17
  |
66 | 65 | toptopon 20025 |
. . . . . . . . . . . . . . . 16

TopOn    |
67 | 4, 66 | sylib 201 |
. . . . . . . . . . . . . . 15
 TopOn    |
68 | 67 | elfvexd 5907 |
. . . . . . . . . . . . . 14
   |
69 | | cnextf.a |
. . . . . . . . . . . . . 14

  |
70 | 68, 69 | ssexd 4543 |
. . . . . . . . . . . . 13
   |
71 | | elrest 15404 |
. . . . . . . . . . . . 13
                        
↾t 
                 |
72 | 64, 70, 71 | syl2anc 673 |
. . . . . . . . . . . 12
            
↾t 
                 |
73 | 72 | biimpa 492 |
. . . . . . . . . . 11
 
           ↾t  
                |
74 | | imaeq2 5170 |
. . . . . . . . . . . . . . 15
          
    |
75 | 74 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                               |
76 | 75 | sseq1d 3445 |
. . . . . . . . . . . . 13
                                 |
77 | 76 | biimpcd 232 |
. . . . . . . . . . . 12
               
             
   |
78 | 77 | reximdv 2857 |
. . . . . . . . . . 11
                           
                             |
79 | 73, 78 | syl5 32 |
. . . . . . . . . 10
                         
↾t   
                            |
80 | 79 | imp 436 |
. . . . . . . . 9
              
          
↾t                                |
81 | 60, 61, 62, 80 | syl12anc 1290 |
. . . . . . . 8
                 CnExt                     ↾t                                            |
82 | | simplll 776 |
. . . . . . . . . . 11
                 CnExt                     CnExt                       |
83 | | simplr 770 |
. . . . . . . . . . 11
                 CnExt                     CnExt                              CnExt           |
84 | | cnextf.6 |
. . . . . . . . . . . . . . . 16
           |
85 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . 19
 
   |
86 | 85 | anbi2d 718 |
. . . . . . . . . . . . . . . . . 18
  

     |
87 | | sneq 3969 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    |
88 | 87 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . 22
                       |
89 | 88 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . 21
           
↾t            
↾t    |
90 | 89 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . 20
             ↾t              
↾t     |
91 | 90 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . 19
             
↾t                  
↾t        |
92 | 91 | neeq1d 2702 |
. . . . . . . . . . . . . . . . . 18
              
↾t     
             ↾t         |
93 | 86, 92 | imbi12d 327 |
. . . . . . . . . . . . . . . . 17
   
             
↾t      
  
             ↾t          |
94 | | cnextf.7 |
. . . . . . . . . . . . . . . . 17
 
             
↾t        |
95 | 93, 94 | chvarv 2120 |
. . . . . . . . . . . . . . . 16
 
             
↾t        |
96 | 65, 46, 4, 32, 37, 69, 84, 95 | cnextfvval 21158 |
. . . . . . . . . . . . . . 15
 
    CnExt                    
↾t        |
97 | | fvex 5889 |
. . . . . . . . . . . . . . . . . 18
 
          
↾t       |
98 | 97 | uniex 6606 |
. . . . . . . . . . . . . . . . 17
             
↾t       |
99 | 98 | snid 3988 |
. . . . . . . . . . . . . . . 16
             
↾t                    
↾t        |
100 | 32 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
   |
101 | 84 | eleq2d 2534 |
. . . . . . . . . . . . . . . . . . . 20
             |
102 | 101 | biimpar 493 |
. . . . . . . . . . . . . . . . . . 19
 
           |
103 | 67 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
 TopOn    |
104 | 69 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
105 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
106 | | trnei 20985 |
. . . . . . . . . . . . . . . . . . . 20
  TopOn           
          
↾t         |
107 | 103, 104,
105, 106 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . 19
 
         
          
↾t         |
108 | 102, 107 | mpbid 215 |
. . . . . . . . . . . . . . . . . 18
 
           
↾t        |
109 | 37 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
       |
110 | 46 | hausflf2 21091 |
. . . . . . . . . . . . . . . . . 18
              ↾t     
                 
↾t                   
↾t        |
111 | 100, 108,
109, 94, 110 | syl31anc 1295 |
. . . . . . . . . . . . . . . . 17
 
             
↾t        |
112 | | en1b 7655 |
. . . . . . . . . . . . . . . . 17
             
↾t                  
↾t                    
↾t         |
113 | 111, 112 | sylib 201 |
. . . . . . . . . . . . . . . 16
 
             
↾t                    
↾t         |
114 | 99, 113 | syl5eleqr 2556 |
. . . . . . . . . . . . . . 15
 
              
↾t                  
↾t        |
115 | 96, 114 | eqeltrd 2549 |
. . . . . . . . . . . . . 14
 
    CnExt                   
↾t        |
116 | 46 | toptopon 20025 |
. . . . . . . . . . . . . . . . 17

TopOn    |
117 | 34, 116 | sylib 201 |
. . . . . . . . . . . . . . . 16
 TopOn    |
118 | 117 | adantr 472 |
. . . . . . . . . . . . . . 15
 
 TopOn    |
119 | | flfnei 21084 |
. . . . . . . . . . . . . . 15
  TopOn            
↾t               CnExt                   
↾t     
    CnExt                   CnExt                     
↾t           |
120 | 118, 108,
109, 119 | syl3anc 1292 |
. . . . . . . . . . . . . 14
 
     CnExt                   
↾t     
    CnExt                   CnExt                     
↾t           |
121 | 115, 120 | mpbid 215 |
. . . . . . . . . . . . 13
 
     CnExt      
            CnExt                     
↾t          |
122 | 121 | simprd 470 |
. . . . . . . . . . . 12
 
             CnExt                     
↾t         |
123 | 122 | r19.21bi 2776 |
. . . . . . . . . . 11
               CnExt         
            ↾t      
  |
124 | 82, 83, 123 | syl2anc 673 |
. . . . . . . . . 10
                 CnExt                     CnExt                               ↾t      
  |
125 | 34 | ad3antrrr 744 |
. . . . . . . . . . . 12
   

           CnExt                     |
126 | | simplr 770 |
. . . . . . . . . . . . 13
   

           CnExt                              CnExt           |
127 | 46 | neii1 20199 |
. . . . . . . . . . . . 13
 
           CnExt            |
128 | 125, 126,
127 | syl2anc 673 |
. . . . . . . . . . . 12
   

           CnExt                     |
129 | | simpr 468 |
. . . . . . . . . . . 12
   

           CnExt                             |
130 | 46 | clsss 20146 |
. . . . . . . . . . . . . . . 16
                             |
131 | | sstr 3426 |
. . . . . . . . . . . . . . . 16
                                             |
132 | 130, 131 | sylan 479 |
. . . . . . . . . . . . . . 15
  
                            |
133 | 132 | 3an1rs 1245 |
. . . . . . . . . . . . . 14
  
                            |
134 | 133 | ex 441 |
. . . . . . . . . . . . 13
               
               |
135 | 134 | reximdv 2857 |
. . . . . . . . . . . 12
            
          
↾t                  
↾t                  |
136 | 125, 128,
129, 135 | syl3anc 1292 |
. . . . . . . . . . 11
   

           CnExt                    
          
↾t                  
↾t                  |
137 | 136 | adantllr 733 |
. . . . . . . . . 10
                 CnExt                     CnExt                    
          
↾t                  
↾t                  |
138 | 124, 137 | mpd 15 |
. . . . . . . . 9
                 CnExt                     CnExt                               ↾t                 |
139 | 34 | ad2antrr 740 |
. . . . . . . . . 10
               CnExt         
  |
140 | | cnextcn.8 |
. . . . . . . . . . . . . . 15
   |
141 | 140 | ad2antrr 740 |
. . . . . . . . . . . . . 14
               CnExt         
  |
142 | 141 | ad2antrr 740 |
. . . . . . . . . . . . 13
                 CnExt               CnExt      
 
  |
143 | | simplr 770 |
. . . . . . . . . . . . 13
                 CnExt               CnExt      
    |
144 | | simprl 772 |
. . . . . . . . . . . . 13
                 CnExt               CnExt      
     CnExt         |
145 | | regsep 20427 |
. . . . . . . . . . . . 13
 
   CnExt        
    CnExt              
   |
146 | 142, 143,
144, 145 | syl3anc 1292 |
. . . . . . . . . . . 12
                 CnExt               CnExt      
  
    CnExt                  |
147 | | sstr 3426 |
. . . . . . . . . . . . . . . 16
                     |
148 | 147 | expcom 442 |
. . . . . . . . . . . . . . 15
         
           |
149 | 148 | anim2d 575 |
. . . . . . . . . . . . . 14
      CnExt                    CnExt      
            |
150 | 149 | reximdv 2857 |
. . . . . . . . . . . . 13
  
    CnExt                
    CnExt              
    |
151 | 150 | ad2antll 743 |
. . . . . . . . . . . 12
                 CnExt               CnExt      
        CnExt              
      CnExt                   |
152 | 146, 151 | mpd 15 |
. . . . . . . . . . 11
                 CnExt               CnExt      
  
    CnExt                  |
153 | | simpr 468 |
. . . . . . . . . . . 12
               CnExt         
           CnExt           |
154 | | neii2 20201 |
. . . . . . . . . . . . 13
 
           CnExt                CnExt       
   |
155 | | fvex 5889 |
. . . . . . . . . . . . . . . . 17
   CnExt        |
156 | 155 | snss 4087 |
. . . . . . . . . . . . . . . 16
    CnExt           CnExt          |
157 | 156 | anbi1i 709 |
. . . . . . . . . . . . . . 15
     CnExt      

     CnExt           |
158 | 157 | biimpri 211 |
. . . . . . . . . . . . . 14
      CnExt       
     CnExt          |
159 | 158 | reximi 2852 |
. . . . . . . . . . . . 13
       CnExt       
      CnExt          |
160 | 154, 159 | syl 17 |
. . . . . . . . . . . 12
 
           CnExt               CnExt          |
161 | 139, 153,
160 | syl2anc 673 |
. . . . . . . . . . 11
               CnExt         

    CnExt          |
162 | 152, 161 | r19.29a 2918 |
. . . . . . . . . 10
               CnExt         

    CnExt              
   |
163 | | anass 661 |
. . . . . . . . . . . 12
      CnExt                

    CnExt      
            |
164 | | opnneip 20212 |
. . . . . . . . . . . . . 14
 
   CnExt                   CnExt           |
165 | 164 | 3expib 1234 |
. . . . . . . . . . . . 13
      CnExt                   CnExt            |
166 | 165 | anim1d 574 |
. . . . . . . . . . . 12
       CnExt                             CnExt                
    |
167 | 163, 166 | syl5bir 226 |
. . . . . . . . . . 11
       CnExt                             CnExt                
    |
168 | 167 | reximdv2 2855 |
. . . . . . . . . 10
  
    CnExt                            CnExt                     |
169 | 139, 162,
168 | sylc 61 |
. . . . . . . . 9
               CnExt         
            CnExt                    |
170 | 138, 169 | r19.29a 2918 |
. . . . . . . 8
               CnExt         
            ↾t                 |
171 | 81, 170 | r19.29a 2918 |
. . . . . . 7
               CnExt         
                            |
172 | 59, 171 | r19.29a 2918 |
. . . . . 6
               CnExt         
                              |
173 | | simplr 770 |
. . . . . . . . . . 11
   
                                 |
174 | | simpll 768 |
. . . . . . . . . . . . 13
       |
175 | 4 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
       |
176 | | simplr 770 |
. . . . . . . . . . . . . . 15
       |
177 | 65 | eltopss 20014 |
. . . . . . . . . . . . . . 15
 

  |
178 | 175, 176,
177 | syl2anc 673 |
. . . . . . . . . . . . . 14
       |
179 | | simpr 468 |
. . . . . . . . . . . . . 14
       |
180 | 178, 179 | sseldd 3419 |
. . . . . . . . . . . . 13
       |
181 | | fvex 5889 |
. . . . . . . . . . . . . . 15
           |
182 | 181 | a1i 11 |
. . . . . . . . . . . . . 14
                 |
183 | 70 | ad2antrr 740 |
. . . . . . . . . . . . . 14
       |
184 | | opnneip 20212 |
. . . . . . . . . . . . . . . 16
 
             |
185 | 4, 184 | syl3an1 1325 |
. . . . . . . . . . . . . . 15
 

            |
186 | 185 | 3expa 1231 |
. . . . . . . . . . . . . 14
                 |
187 | | elrestr 15405 |
. . . . . . . . . . . . . 14
           
          
            
↾t    |
188 | 182, 183,
186, 187 | syl3anc 1292 |
. . . . . . . . . . . . 13
     
            ↾t    |
189 | 65, 46, 4, 32, 37, 69, 84, 94 | cnextfvval 21158 |
. . . . . . . . . . . . . . 15
 
    CnExt                    
↾t        |
190 | 189 | adantr 472 |
. . . . . . . . . . . . . 14
    
            ↾t  
   CnExt                    
↾t        |
191 | 32 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
   |
192 | 84 | eleq2d 2534 |
. . . . . . . . . . . . . . . . . . . . 21
             |
193 | 192 | biimpar 493 |
. . . . . . . . . . . . . . . . . . . 20
 
           |
194 | 67 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
 
 TopOn    |
195 | 69 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
196 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
197 | | trnei 20985 |
. . . . . . . . . . . . . . . . . . . . 21
  TopOn           
          
↾t         |
198 | 194, 195,
196, 197 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . 20
 
         
          
↾t         |
199 | 193, 198 | mpbid 215 |
. . . . . . . . . . . . . . . . . . 19
 
           
↾t        |
200 | 37 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
       |
201 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
202 | 201 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . . 21
  

     |
203 | | sneq 3969 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
    |
204 | 203 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                       |
205 | 204 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
↾t            
↾t    |
206 | 205 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . 23
             ↾t              
↾t     |
207 | 206 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . . . . 22
             
↾t                  
↾t        |
208 | 207 | neeq1d 2702 |
. . . . . . . . . . . . . . . . . . . . 21
              
↾t     
             ↾t         |
209 | 202, 208 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . 20
   
             
↾t      
  
             ↾t          |
210 | 209, 94 | chvarv 2120 |
. . . . . . . . . . . . . . . . . . 19
 
             
↾t        |
211 | 46 | hausflf2 21091 |
. . . . . . . . . . . . . . . . . . 19
              ↾t     
                 
↾t                   
↾t        |
212 | 191, 199,
200, 210, 211 | syl31anc 1295 |
. . . . . . . . . . . . . . . . . 18
 
             
↾t        |
213 | | en1b 7655 |
. . . . . . . . . . . . . . . . . 18
             
↾t                  
↾t                    
↾t         |
214 | 212, 213 | sylib 201 |
. . . . . . . . . . . . . . . . 17
 
             
↾t                    
↾t         |
215 | 214 | adantr 472 |
. . . . . . . . . . . . . . . 16
    
            ↾t  
             ↾t                    
↾t         |
216 | 117 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
 TopOn    |
217 | | flfval 21083 |
. . . . . . . . . . . . . . . . . . 19
  TopOn            
↾t                       
↾t      
                ↾t      |
218 | 216, 199,
200, 217 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
 
             
↾t      
                ↾t      |
219 | 218 | adantr 472 |
. . . . . . . . . . . . . . . . 17
    
            ↾t  
             ↾t      
                ↾t      |
220 | | uniexg 6607 |
. . . . . . . . . . . . . . . . . . . . . 22

   |
221 | 32, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
    |
222 | 221 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . 20
    
            ↾t  
   |
223 | 46, 222 | syl5eqel 2553 |
. . . . . . . . . . . . . . . . . . 19
    
            ↾t  
  |
224 | 199 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
    
            ↾t  
          
↾t        |
225 | | filfbas 20941 |
. . . . . . . . . . . . . . . . . . . 20
           
↾t                 ↾t        |
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    
            ↾t  
          
↾t        |
227 | 37 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
    
            ↾t  
      |
228 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . 20
    
            ↾t  
            
↾t    |
229 | | fgfil 20968 |
. . . . . . . . . . . . . . . . . . . . . 22
           
↾t                   
↾t              ↾t    |
230 | 199, 229 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
               ↾t              ↾t    |
231 | 230 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
    
            ↾t  
              ↾t             
↾t    |
232 | 228, 231 | eleqtrrd 2552 |
. . . . . . . . . . . . . . . . . . 19
    
            ↾t  
                ↾t     |
233 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . 20
              ↾t                 ↾t    |
234 | 233 | imaelfm 21044 |
. . . . . . . . . . . . . . . . . . 19
              ↾t     
     
              
↾t                          ↾t     |
235 | 223, 226,
227, 232, 234 | syl31anc 1295 |
. . . . . . . . . . . . . . . . . 18
    
            ↾t  
                      ↾t     |
236 | | flimclsi 21071 |
. . . . . . . . . . . . . . . . . 18
                      
↾t                    ↾t                    |
237 | 235, 236 | syl 17 |
. . . . . . . . . . . . . . . . 17
    
            ↾t  
                
↾t                    |
238 | 219, 237 | eqsstrd 3452 |
. . . . . . . . . . . . . . . 16
    
            ↾t  
             ↾t                      |
239 | 215, 238 | eqsstr3d 3453 |
. . . . . . . . . . . . . . 15
    
            ↾t  
              
↾t                       |
240 | | fvex 5889 |
. . . . . . . . . . . . . . . . 17
 
          
↾t       |
241 | 240 | uniex 6606 |
. . . . . . . . . . . . . . . 16
             
↾t       |
242 | 241 | snss 4087 |
. . . . . . . . . . . . . . 15
              
↾t                   
              
↾t                       |
243 | 239, 242 | sylibr 217 |
. . . . . . . . . . . . . 14
    
            ↾t  
             
↾t                      |
244 | 190, 243 | eqeltrd 2549 |
. . . . . . . . . . . . 13
    
            ↾t  
   CnExt                       |
245 | 174, 180,
188, 244 | syl21anc 1291 |
. . . . . . . . . . . 12
        CnExt                       |
246 | 245 | adantlr 729 |
. . . . . . . . . . 11
   
                    CnExt                       |
247 | 173, 246 | sseldd 3419 |
. . . . . . . . . 10
   
                    CnExt         |
248 | 247 | ralrimiva 2809 |
. . . . . . . . 9
                   
   CnExt         |
249 | 248 | expl 630 |
. . . . . . . 8
                  
   CnExt          |
250 | 249 | reximdv 2857 |
. . . . . . 7
                                          
   CnExt          |
251 | 250 | ad2antrr 740 |
. . . . . 6
               CnExt         
 
                                       
   CnExt          |
252 | 172, 251 | mpd 15 |
. . . . 5
               CnExt         
            
   CnExt         |
253 | 65, 46, 4, 32, 37, 69, 84, 94 | cnextf 21159 |
. . . . . . . . . 10
   CnExt          |
254 | | ffun 5742 |
. . . . . . . . . 10
   CnExt          CnExt      |
255 | 253, 254 | syl 17 |
. . . . . . . . 9
   CnExt      |
256 | 255 | adantr 472 |
. . . . . . . 8
 
             CnExt      |
257 | 65 | neii1 20199 |
. . . . . . . . . 10
 
          
  |
258 | 4, 257 | sylan 479 |
. . . . . . . . 9
 
          
  |
259 | | fdm 5745 |
. . . . . . . . . . 11
   CnExt          CnExt      |
260 | 253, 259 | syl 17 |
. . . . . . . . . 10
   CnExt      |
261 | 260 | adantr 472 |
. . . . . . . . 9
 
             CnExt      |
262 | 258, 261 | sseqtr4d 3455 |
. . . . . . . 8
 
          
  CnExt      |
263 | | funimass4 5930 |
. . . . . . . 8
    CnExt   
  CnExt    
    CnExt           CnExt          |
264 | 256, 262,
263 | syl2anc 673 |
. . . . . . 7
 
               CnExt      

   CnExt          |
265 | 264 | biimprd 231 |
. . . . . 6
 
                CnExt          CnExt          |
266 | 265 | reximdva 2858 |
. . . . 5
              
   CnExt                      CnExt          |
267 | 1, 252, 266 | sylc 61 |
. . . 4
               CnExt         
               CnExt         |
268 | 267 | ralrimiva 2809 |
. . 3
 
             CnExt                         CnExt         |
269 | 268 | ralrimiva 2809 |
. 2
  
           CnExt                         CnExt         |
270 | 65, 46 | cnnei 20375 |
. . 3
 
  CnExt            CnExt     

            CnExt                         CnExt          |
271 | 4, 34, 253, 270 | syl3anc 1292 |
. 2
    CnExt     

            CnExt                         CnExt          |
272 | 269, 271 | mpbird 240 |
1
   CnExt        |