Step | Hyp | Ref
| Expression |
1 | | nfv 1769 |
. . . . . 6
  
  |
2 | | nfv 1769 |
. . . . . . 7

  ↾t   |
3 | | nfre1 2846 |
. . . . . . 7
    ↾t      |
4 | 2, 3 | nfan 2031 |
. . . . . 6
     ↾t  
 ↾t       |
5 | 1, 4 | nfan 2031 |
. . . . 5
   
   
↾t  
 ↾t        |
6 | | simpl 464 |
. . . . . . 7
 
  ↾t  
 ↾t        ↾t    |
7 | 6 | anim2i 579 |
. . . . . 6
  
    ↾t  
 ↾t        
   ↾t     |
8 | | simp-5r 787 |
. . . . . . . . . . 11
      
   ↾t   
↾t   
  
     ↾t    |
9 | | simp1 1030 |
. . . . . . . . . . . . 13
     |
10 | | simp2 1031 |
. . . . . . . . . . . . 13
     |
11 | | neitr.1 |
. . . . . . . . . . . . . 14
  |
12 | 11 | restuni 20255 |
. . . . . . . . . . . . 13
  
  ↾t    |
13 | 9, 10, 12 | syl2anc 673 |
. . . . . . . . . . . 12
     ↾t    |
14 | 13 | ad5antr 748 |
. . . . . . . . . . 11
      
   ↾t   
↾t   
  
     ↾t    |
15 | 8, 14 | sseqtr4d 3455 |
. . . . . . . . . 10
      
   ↾t   
↾t   
  
     |
16 | 10 | ad5antr 748 |
. . . . . . . . . 10
      
   ↾t   
↾t   
  
     |
17 | 15, 16 | sstrd 3428 |
. . . . . . . . 9
      
   ↾t   
↾t   
  
     |
18 | 9 | ad5antr 748 |
. . . . . . . . . . 11
      
   ↾t   
↾t   
  
     |
19 | | simplr 770 |
. . . . . . . . . . 11
      
   ↾t   
↾t   
  
     |
20 | 11 | eltopss 20014 |
. . . . . . . . . . 11
 

  |
21 | 18, 19, 20 | syl2anc 673 |
. . . . . . . . . 10
      
   ↾t   
↾t   
  
     |
22 | 21 | ssdifssd 3560 |
. . . . . . . . 9
      
   ↾t   
↾t   
  
   
   |
23 | 17, 22 | unssd 3601 |
. . . . . . . 8
      
   ↾t   
↾t   
  
         |
24 | | simpr1l 1087 |
. . . . . . . . . . . 12
        ↾t   
↾t     
      |
25 | 24 | 3anassrs 1256 |
. . . . . . . . . . 11
      
   ↾t   
↾t   
  
     |
26 | | simpr 468 |
. . . . . . . . . . 11
      
   ↾t   
↾t   
  
       |
27 | 25, 26 | sseqtrd 3454 |
. . . . . . . . . 10
      
   ↾t   
↾t   
  
       |
28 | | inss1 3643 |
. . . . . . . . . 10
   |
29 | 27, 28 | syl6ss 3430 |
. . . . . . . . 9
      
   ↾t   
↾t   
  
     |
30 | | inundif 3836 |
. . . . . . . . . 10
       |
31 | | simpr1r 1088 |
. . . . . . . . . . . . 13
        ↾t   
↾t     
      |
32 | 31 | 3anassrs 1256 |
. . . . . . . . . . . 12
      
   ↾t   
↾t   
  
     |
33 | 26, 32 | eqsstr3d 3453 |
. . . . . . . . . . 11
      
   ↾t   
↾t   
  
   
   |
34 | | unss1 3594 |
. . . . . . . . . . 11
               |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
      
   ↾t   
↾t   
  
               |
36 | 30, 35 | syl5eqssr 3463 |
. . . . . . . . 9
      
   ↾t   
↾t   
  
    
    |
37 | | sseq2 3440 |
. . . . . . . . . . 11
 
   |
38 | | sseq1 3439 |
. . . . . . . . . . 11
 
   
 
     |
39 | 37, 38 | anbi12d 725 |
. . . . . . . . . 10
  
     
        |
40 | 39 | rspcev 3136 |
. . . . . . . . 9
  
       
       |
41 | 19, 29, 36, 40 | syl12anc 1290 |
. . . . . . . 8
      
   ↾t   
↾t   
  
   
  
     |
42 | | indir 3682 |
. . . . . . . . . . 11
           
   |
43 | | incom 3616 |
. . . . . . . . . . . . 13
         |
44 | | disjdif 3830 |
. . . . . . . . . . . . 13
     |
45 | 43, 44 | eqtr3i 2495 |
. . . . . . . . . . . 12
     |
46 | 45 | uneq2i 3576 |
. . . . . . . . . . 11
             |
47 | | un0 3762 |
. . . . . . . . . . 11
       |
48 | 42, 46, 47 | 3eqtri 2497 |
. . . . . . . . . 10
         |
49 | | df-ss 3404 |
. . . . . . . . . . 11

    |
50 | 49 | biimpi 199 |
. . . . . . . . . 10
 
   |
51 | 48, 50 | syl5req 2518 |
. . . . . . . . 9
         |
52 | 15, 51 | syl 17 |
. . . . . . . 8
      
   ↾t   
↾t   
  
           |
53 | | vex 3034 |
. . . . . . . . . 10
 |
54 | | vex 3034 |
. . . . . . . . . . 11
 |
55 | | difexg 4545 |
. . . . . . . . . . 11
 
   |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . 10
   |
57 | 53, 56 | unex 6608 |
. . . . . . . . 9
     |
58 | | sseq1 3439 |
. . . . . . . . . . 11
     
       |
59 | | sseq2 3440 |
. . . . . . . . . . . . 13
     
 
     |
60 | 59 | anbi2d 718 |
. . . . . . . . . . . 12
      
 
        |
61 | 60 | rexbidv 2892 |
. . . . . . . . . . 11
      



  
      |
62 | 58, 61 | anbi12d 725 |
. . . . . . . . . 10
        
        
         |
63 | | ineq1 3618 |
. . . . . . . . . . 11
     
         |
64 | 63 | eqeq2d 2481 |
. . . . . . . . . 10
       
         |
65 | 62, 64 | anbi12d 725 |
. . . . . . . . 9
              
   
 
 
        
 
     |
66 | 57, 65 | spcev 3127 |
. . . . . . . 8
        
        
 
 
             |
67 | 23, 41, 52, 66 | syl21anc 1291 |
. . . . . . 7
      
   ↾t   
↾t   
  
                |
68 | 9 | ad3antrrr 744 |
. . . . . . . 8
        ↾t   
↾t   
    |
69 | | uniexg 6607 |
. . . . . . . . . . . 12
    |
70 | 9, 69 | syl 17 |
. . . . . . . . . . 11
      |
71 | 11, 70 | syl5eqel 2553 |
. . . . . . . . . 10
     |
72 | 71, 10 | ssexd 4543 |
. . . . . . . . 9
     |
73 | 72 | ad3antrrr 744 |
. . . . . . . 8
        ↾t   
↾t   
    |
74 | | simplr 770 |
. . . . . . . 8
        ↾t   
↾t   
   ↾t    |
75 | | elrest 15404 |
. . . . . . . . 9
 
   ↾t 

     |
76 | 75 | biimpa 492 |
. . . . . . . 8
   
 ↾t   
    |
77 | 68, 73, 74, 76 | syl21anc 1291 |
. . . . . . 7
        ↾t   
↾t   
  
    |
78 | 67, 77 | r19.29a 2918 |
. . . . . 6
        ↾t   
↾t   
     
 
       |
79 | 7, 78 | sylanl1 662 |
. . . . 5
      
  ↾t  
 ↾t      
 ↾t          
  
     |
80 | | simprr 774 |
. . . . 5
  
    ↾t  
 ↾t       
 ↾t       |
81 | 5, 79, 80 | r19.29af 2916 |
. . . 4
  
    ↾t  
 ↾t           
  
     |
82 | | inss2 3644 |
. . . . . . . . . 10
   |
83 | | sseq1 3439 |
. . . . . . . . . 10
   
     |
84 | 82, 83 | mpbiri 241 |
. . . . . . . . 9
     |
85 | 84 | adantl 473 |
. . . . . . . 8
    
    
  |
86 | 85 | exlimiv 1784 |
. . . . . . 7
     
  
  
  |
87 | 86 | adantl 473 |
. . . . . 6
  
     
  
      |
88 | 13 | adantr 472 |
. . . . . 6
  
     
  
     
↾t    |
89 | 87, 88 | sseqtrd 3454 |
. . . . 5
  
     
  
      ↾t    |
90 | 9 | ad4antr 746 |
. . . . . . . . . . . . . . 15
          
 
 
  |
91 | 72 | ad4antr 746 |
. . . . . . . . . . . . . . 15
          
 
 
  |
92 | | simplr 770 |
. . . . . . . . . . . . . . 15
          
 
 
  |
93 | | elrestr 15405 |
. . . . . . . . . . . . . . 15
 
 
 
↾t    |
94 | 90, 91, 92, 93 | syl3anc 1292 |
. . . . . . . . . . . . . 14
          
 
 
   ↾t    |
95 | | simprl 772 |
. . . . . . . . . . . . . . 15
          
 
 
  |
96 | | simp3 1032 |
. . . . . . . . . . . . . . . 16
     |
97 | 96 | ad4antr 746 |
. . . . . . . . . . . . . . 15
          
 
 
  |
98 | 95, 97 | ssind 3647 |
. . . . . . . . . . . . . 14
          
 
 

   |
99 | | simprr 774 |
. . . . . . . . . . . . . . . 16
          
 
 
  |
100 | | ssrin 3648 |
. . . . . . . . . . . . . . . 16
 
     |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . 15
          
 
 
  
   |
102 | | simp-4r 785 |
. . . . . . . . . . . . . . 15
          
 
 
    |
103 | 101, 102 | sseqtr4d 3455 |
. . . . . . . . . . . . . 14
          
 
 
    |
104 | 94, 98, 103 | jca32 544 |
. . . . . . . . . . . . 13
          
 
 
 
 
↾t     
     |
105 | 104 | ex 441 |
. . . . . . . . . . . 12
         
   
 
 
↾t     
      |
106 | 105 | reximdva 2858 |
. . . . . . . . . . 11
   
      

 
    ↾t     
      |
107 | 106 | impr 631 |
. . . . . . . . . 10
   
     
         ↾t     
     |
108 | 107 | an32s 821 |
. . . . . . . . 9
   
      
   
    ↾t     
     |
109 | 108 | expl 630 |
. . . . . . . 8
             
    ↾t     
      |
110 | 109 | exlimdv 1787 |
. . . . . . 7
        
  
   
    ↾t     
      |
111 | 110 | imp 436 |
. . . . . 6
  
     
  
         ↾t     
     |
112 | | sseq2 3440 |
. . . . . . . . 9
   

    |
113 | | sseq1 3439 |
. . . . . . . . 9
   
     |
114 | 112, 113 | anbi12d 725 |
. . . . . . . 8
    
  
  
    |
115 | 114 | rspcev 3136 |
. . . . . . 7
     ↾t     
   
 ↾t       |
116 | 115 | rexlimivw 2869 |
. . . . . 6
      ↾t     
   
 ↾t       |
117 | 111, 116 | syl 17 |
. . . . 5
  
     
  
      ↾t       |
118 | 89, 117 | jca 541 |
. . . 4
  
     
  
      
↾t  
 ↾t        |
119 | 81, 118 | impbida 850 |
. . 3
       ↾t  
 ↾t     
              |
120 | | resttop 20253 |
. . . . 5
 
 
↾t    |
121 | 9, 72, 120 | syl2anc 673 |
. . . 4
    ↾t    |
122 | 96, 13 | sseqtrd 3454 |
. . . 4
     ↾t    |
123 | | eqid 2471 |
. . . . 5
  ↾t   
↾t   |
124 | 123 | isnei 20196 |
. . . 4
  
↾t 
  ↾t         ↾t     
   ↾t   
↾t         |
125 | 121, 122,
124 | syl2anc 673 |
. . 3
         ↾t        
↾t  
 ↾t         |
126 | | fvex 5889 |
. . . . . 6
         |
127 | | restval 15403 |
. . . . . 6
                    ↾t                |
128 | 126, 72, 127 | sylancr 676 |
. . . . 5
            ↾t                |
129 | 128 | eleq2d 2534 |
. . . 4
             ↾t                 |
130 | 96, 10 | sstrd 3428 |
. . . . 5
     |
131 | | eqid 2471 |
. . . . . . . . 9
                         |
132 | 131 | elrnmpt 5087 |
. . . . . . . 8
                             |
133 | 53, 132 | ax-mp 5 |
. . . . . . 7
            
              |
134 | | df-rex 2762 |
. . . . . . 7
            
          

    |
135 | 133, 134 | bitri 257 |
. . . . . 6
            
          

    |
136 | 11 | isnei 20196 |
. . . . . . . 8
            
 
     |
137 | 136 | anbi1d 719 |
. . . . . . 7
            

    
  
      |
138 | 137 | exbidv 1776 |
. . . . . 6
              
  
              |
139 | 135, 138 | syl5bb 265 |
. . . . 5
               
              |
140 | 9, 130, 139 | syl2anc 673 |
. . . 4
                   
 
        |
141 | 129, 140 | bitrd 261 |
. . 3
             ↾t     
 
        |
142 | 119, 125,
141 | 3bitr4d 293 |
. 2
         ↾t               ↾t     |
143 | 142 | eqrdv 2469 |
1
        ↾t               ↾t    |