Proof of Theorem ressress
Step | Hyp | Ref
| Expression |
1 | | simplr 763 |
. . . . . . . . 9
      
↾s       
      
  |
2 | | simpr1 1015 |
. . . . . . . . 9
      
↾s       
  
  |
3 | | simpr2 1016 |
. . . . . . . . 9
      
↾s       
  
  |
4 | | eqid 2453 |
. . . . . . . . . 10
 ↾s   ↾s   |
5 | | eqid 2453 |
. . . . . . . . . 10
         |
6 | 4, 5 | ressval2 15190 |
. . . . . . . . 9
     
  ↾s   sSet      
          |
7 | 1, 2, 3, 6 | syl3anc 1269 |
. . . . . . . 8
      
↾s       
   
↾s   sSet      
          |
8 | | inass 3644 |
. . . . . . . . . . 11
                 |
9 | | in12 3645 |
. . . . . . . . . . 11
                 |
10 | 8, 9 | eqtri 2475 |
. . . . . . . . . 10
                 |
11 | 4, 5 | ressbas 15191 |
. . . . . . . . . . . 12
           ↾s     |
12 | 3, 11 | syl 17 |
. . . . . . . . . . 11
      
↾s       
             ↾s     |
13 | 12 | ineq2d 3636 |
. . . . . . . . . 10
      
↾s       
                ↾s      |
14 | 10, 13 | syl5req 2500 |
. . . . . . . . 9
      
↾s       
        ↾s      
       |
15 | 14 | opeq2d 4176 |
. . . . . . . 8
      
↾s       
        
     ↾s    
        
        |
16 | 7, 15 | oveq12d 6313 |
. . . . . . 7
      
↾s       
     ↾s  sSet      
     ↾s     
  sSet
              sSet      
            |
17 | | fvex 5880 |
. . . . . . . . 9
     |
18 | 17 | inex2 4548 |
. . . . . . . 8
         |
19 | | setsabs 15164 |
. . . . . . . 8
             sSet
              sSet      
           sSet                   |
20 | 2, 18, 19 | sylancl 669 |
. . . . . . 7
      
↾s       
     sSet              
sSet         
        sSet      
            |
21 | 16, 20 | eqtrd 2487 |
. . . . . 6
      
↾s       
     ↾s  sSet      
     ↾s     
 sSet      
            |
22 | | simpll 761 |
. . . . . . 7
      
↾s       
       ↾s     |
23 | | ovex 6323 |
. . . . . . . 8
 ↾s   |
24 | 23 | a1i 11 |
. . . . . . 7
      
↾s       
   
↾s    |
25 | | simpr3 1017 |
. . . . . . 7
      
↾s       
  
  |
26 | | eqid 2453 |
. . . . . . . 8
  ↾s 
↾s   
↾s 
↾s   |
27 | | eqid 2453 |
. . . . . . . 8
   
↾s       ↾s    |
28 | 26, 27 | ressval2 15190 |
. . . . . . 7
      ↾s    ↾s    
↾s 
↾s   
↾s  sSet            ↾s        |
29 | 22, 24, 25, 28 | syl3anc 1269 |
. . . . . 6
      
↾s       
     ↾s  ↾s    ↾s  sSet            ↾s        |
30 | | inss1 3654 |
. . . . . . . . 9
   |
31 | | sstr 3442 |
. . . . . . . . 9
     
           |
32 | 30, 31 | mpan2 678 |
. . . . . . . 8
      
      |
33 | 1, 32 | nsyl 125 |
. . . . . . 7
      
↾s       
      
    |
34 | | inex1g 4549 |
. . . . . . . 8
     |
35 | 3, 34 | syl 17 |
. . . . . . 7
      
↾s       
       |
36 | | eqid 2453 |
. . . . . . . 8
 ↾s     ↾s     |
37 | 36, 5 | ressval2 15190 |
. . . . . . 7
     
      ↾s 
   sSet      
            |
38 | 33, 2, 35, 37 | syl3anc 1269 |
. . . . . 6
      
↾s       
   
↾s     sSet      
            |
39 | 21, 29, 38 | 3eqtr4d 2497 |
. . . . 5
      
↾s       
     ↾s  ↾s   ↾s      |
40 | 39 | exp31 609 |
. . . 4
     ↾s         
  
↾s 
↾s   ↾s        |
41 | 26, 27 | ressid2 15189 |
. . . . . . . 8
      ↾s    ↾s    
↾s 
↾s   ↾s    |
42 | 23, 41 | mp3an2 1354 |
. . . . . . 7
      ↾s   
  ↾s 
↾s   ↾s    |
43 | 42 | 3ad2antr3 1176 |
. . . . . 6
      ↾s   
   
↾s 
↾s   ↾s    |
44 | | in32 3646 |
. . . . . . . . 9
                 |
45 | | simpr2 1016 |
. . . . . . . . . . . 12
      ↾s   
    |
46 | 45, 11 | syl 17 |
. . . . . . . . . . 11
      ↾s   
            ↾s     |
47 | | simpl 459 |
. . . . . . . . . . 11
      ↾s   
      ↾s  
  |
48 | 46, 47 | eqsstrd 3468 |
. . . . . . . . . 10
      ↾s   
          |
49 | | df-ss 3420 |
. . . . . . . . . 10
             
         |
50 | 48, 49 | sylib 200 |
. . . . . . . . 9
      ↾s   
                  |
51 | 44, 50 | syl5req 2500 |
. . . . . . . 8
      ↾s   
          
       |
52 | 51 | oveq2d 6311 |
. . . . . . 7
      ↾s   
   ↾s 
       ↾s   
        |
53 | 5 | ressinbas 15197 |
. . . . . . . 8
  ↾s   ↾s          |
54 | 45, 53 | syl 17 |
. . . . . . 7
      ↾s   
   ↾s   ↾s          |
55 | 5 | ressinbas 15197 |
. . . . . . . 8
    ↾s 
   ↾s   
        |
56 | 45, 34, 55 | 3syl 18 |
. . . . . . 7
      ↾s   
   ↾s 
   ↾s   
        |
57 | 52, 54, 56 | 3eqtr4d 2497 |
. . . . . 6
      ↾s   
   ↾s   ↾s      |
58 | 43, 57 | eqtrd 2487 |
. . . . 5
      ↾s   
   
↾s 
↾s   ↾s      |
59 | 58 | ex 436 |
. . . 4
     ↾s    

  ↾s 
↾s   ↾s       |
60 | 4, 5 | ressid2 15189 |
. . . . . . . 8
     
  ↾s    |
61 | 60 | 3adant3r3 1220 |
. . . . . . 7
     

 
 ↾s    |
62 | 61 | oveq1d 6310 |
. . . . . 6
     

 
  ↾s 
↾s   ↾s    |
63 | | inss2 3655 |
. . . . . . . . . . 11
           |
64 | | simpl 459 |
. . . . . . . . . . 11
     

 
      |
65 | 63, 64 | syl5ss 3445 |
. . . . . . . . . 10
     

 
        |
66 | | sseqin2 3653 |
. . . . . . . . . 10
                       |
67 | 65, 66 | sylib 200 |
. . . . . . . . 9
     

 
                |
68 | 8, 67 | syl5req 2500 |
. . . . . . . 8
     

 
        
       |
69 | 68 | oveq2d 6311 |
. . . . . . 7
     

 
 ↾s        
↾s            |
70 | | simpr3 1017 |
. . . . . . . 8
     

 
  |
71 | 5 | ressinbas 15197 |
. . . . . . . 8
  ↾s   ↾s          |
72 | 70, 71 | syl 17 |
. . . . . . 7
     

 
 ↾s   ↾s          |
73 | | simpr2 1016 |
. . . . . . . 8
     

 
  |
74 | 73, 34, 55 | 3syl 18 |
. . . . . . 7
     

 
 ↾s     ↾s            |
75 | 69, 72, 74 | 3eqtr4d 2497 |
. . . . . 6
     

 
 ↾s   ↾s      |
76 | 62, 75 | eqtrd 2487 |
. . . . 5
     

 
  ↾s 
↾s   ↾s      |
77 | 76 | ex 436 |
. . . 4
    
 
  
↾s 
↾s   ↾s       |
78 | 40, 59, 77 | pm2.61ii 169 |
. . 3
 
   ↾s  ↾s   ↾s      |
79 | 78 | 3expib 1212 |
. 2
  

  ↾s 
↾s   ↾s       |
80 | | ress0 15195 |
. . . 4
 ↾s   |
81 | | reldmress 15187 |
. . . . . 6
↾s |
82 | 81 | ovprc1 6326 |
. . . . 5
  ↾s    |
83 | 82 | oveq1d 6310 |
. . . 4
  
↾s 
↾s   ↾s    |
84 | 81 | ovprc1 6326 |
. . . 4
  ↾s      |
85 | 80, 83, 84 | 3eqtr4a 2513 |
. . 3
  
↾s 
↾s   ↾s      |
86 | 85 | a1d 26 |
. 2
  

  ↾s 
↾s   ↾s       |
87 | 79, 86 | pm2.61i 168 |
1
 
   ↾s  ↾s   ↾s      |