Step | Hyp | Ref
| Expression |
1 | | orc 392 |
. . 3
                 |
2 | 1 | a1i 11 |
. 2
                   |
3 | | olc 391 |
. . 3
                 |
4 | 3 | a1i 11 |
. 2
                   |
5 | | funcres2c.a |
. . . . 5
     |
6 | | eqid 2471 |
. . . . 5
       |
7 | | eqid 2471 |
. . . . . . 7
         |
8 | | eqid 2471 |
. . . . . . 7
 f    f    |
9 | | funcres2c.d |
. . . . . . 7
   |
10 | | inss2 3644 |
. . . . . . . 8
           |
11 | 10 | a1i 11 |
. . . . . . 7
             |
12 | 7, 8, 9, 11 | fullsubc 15833 |
. . . . . 6
   f
                 Subcat    |
13 | 12 | adantr 472 |
. . . . 5
 
             f                  Subcat    |
14 | 8, 7 | homffn 15676 |
. . . . . . 7
 f              |
15 | | xpss12 4945 |
. . . . . . . 8
           
                                     |
16 | 10, 10, 15 | mp2an 686 |
. . . . . . 7
             
           |
17 | | fnssres 5699 |
. . . . . . 7
  
f                                        f                                  |
18 | 14, 16, 17 | mp2an 686 |
. . . . . 6
  f                                 |
19 | 18 | a1i 11 |
. . . . 5
 
             f                                  |
20 | | funcres2c.1 |
. . . . . . . 8
       |
21 | 20 | adantr 472 |
. . . . . . 7
 
                 |
22 | | ffn 5739 |
. . . . . . 7
    
  |
23 | 21, 22 | syl 17 |
. . . . . 6
 
             |
24 | | frn 5747 |
. . . . . . . 8
    
  |
25 | 21, 24 | syl 17 |
. . . . . . 7
 
          
  |
26 | | simpr 468 |
. . . . . . . . . 10
 
    
      |
27 | 5, 7, 26 | funcf1 15849 |
. . . . . . . . 9
 
    
          |
28 | | frn 5747 |
. . . . . . . . 9
               |
29 | 27, 28 | syl 17 |
. . . . . . . 8
 
    
      |
30 | | eqid 2471 |
. . . . . . . . . . 11
         |
31 | | simpr 468 |
. . . . . . . . . . 11
 
    
      |
32 | 5, 30, 31 | funcf1 15849 |
. . . . . . . . . 10
 
    
          |
33 | | frn 5747 |
. . . . . . . . . 10
               |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
 
    
      |
35 | | funcres2c.e |
. . . . . . . . . 10

↾s   |
36 | 35, 7 | ressbasss 15259 |
. . . . . . . . 9
         |
37 | 34, 36 | syl6ss 3430 |
. . . . . . . 8
 
    
      |
38 | 29, 37 | jaodan 802 |
. . . . . . 7
 
          
      |
39 | 25, 38 | ssind 3647 |
. . . . . 6
 
          
        |
40 | | df-f 5593 |
. . . . . 6
          

         |
41 | 23, 39, 40 | sylanbrc 677 |
. . . . 5
 
               
       |
42 | | eqid 2471 |
. . . . . . . . 9
       |
43 | | simpr 468 |
. . . . . . . . 9
   
 
    
      |
44 | | simplrl 778 |
. . . . . . . . 9
   
 
    
  |
45 | | simplrr 779 |
. . . . . . . . 9
   
 
    
  |
46 | 5, 6, 42, 43, 44, 45 | funcf2 15851 |
. . . . . . . 8
   
 
    
                                |
47 | | eqid 2471 |
. . . . . . . . . 10
       |
48 | | simpr 468 |
. . . . . . . . . 10
   
 
    
      |
49 | | simplrl 778 |
. . . . . . . . . 10
   
 
    
  |
50 | | simplrr 779 |
. . . . . . . . . 10
   
 
    
  |
51 | 5, 6, 47, 48, 49, 50 | funcf2 15851 |
. . . . . . . . 9
   
 
    
                                |
52 | | funcres2c.r |
. . . . . . . . . . . . 13
   |
53 | 35, 42 | resshom 15394 |
. . . . . . . . . . . . 13
         |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . 12
         |
55 | 54 | ad2antrr 740 |
. . . . . . . . . . 11
   
 
    
        |
56 | 55 | oveqd 6325 |
. . . . . . . . . 10
   
 
    
      
                         |
57 | 56 | feq3d 5726 |
. . . . . . . . 9
   
 
    
                              
                                 |
58 | 51, 57 | mpbird 240 |
. . . . . . . 8
   
 
    
                                |
59 | 46, 58 | jaodan 802 |
. . . . . . 7
   
 
                                           |
60 | 59 | an32s 821 |
. . . . . 6
                                                 |
61 | 41 | adantr 472 |
. . . . . . . . . 10
                             |
62 | | simprl 772 |
. . . . . . . . . 10
                
  |
63 | 61, 62 | ffvelrnd 6038 |
. . . . . . . . 9
                             |
64 | | simprr 774 |
. . . . . . . . . 10
                   |
65 | 61, 64 | ffvelrnd 6038 |
. . . . . . . . 9
                             |
66 | 63, 65 | ovresd 6456 |
. . . . . . . 8
                         f                              
f           |
67 | 10, 63 | sseldi 3416 |
. . . . . . . . 9
                           |
68 | 10, 65 | sseldi 3416 |
. . . . . . . . 9
                           |
69 | 8, 7, 42, 67, 68 | homfval 15675 |
. . . . . . . 8
                        f                          |
70 | 66, 69 | eqtrd 2505 |
. . . . . . 7
                         f                                         |
71 | 70 | feq3d 5726 |
. . . . . 6
                                         f                                                         |
72 | 60, 71 | mpbird 240 |
. . . . 5
                                        f                          |
73 | 5, 6, 13, 19, 41, 72 | funcres2b 15880 |
. . . 4
 
             
     cat   f
                       |
74 | | eqidd 2472 |
. . . . . 6
 
            f
   f
    |
75 | | eqidd 2472 |
. . . . . 6
 
           compf  compf    |
76 | 7 | ressinbas 15263 |
. . . . . . . . . . 11
  ↾s   ↾s          |
77 | 52, 76 | syl 17 |
. . . . . . . . . 10
 
↾s   ↾s          |
78 | 35, 77 | syl5eq 2517 |
. . . . . . . . 9
  ↾s          |
79 | 78 | fveq2d 5883 |
. . . . . . . 8
 
f   
f   ↾s           |
80 | | eqid 2471 |
. . . . . . . . . 10
 ↾s         ↾s         |
81 | | eqid 2471 |
. . . . . . . . . 10
 cat   f
                   cat   f
                   |
82 | 7, 8, 9, 11, 80, 81 | fullresc 15834 |
. . . . . . . . 9
   f
  ↾s          f  
cat   f
                   compf  ↾s 
       compf 
cat   f
                      |
83 | 82 | simpld 466 |
. . . . . . . 8
 
f   ↾s          f
  cat   f
                     |
84 | 79, 83 | eqtrd 2505 |
. . . . . . 7
 
f   
f   cat  
f                      |
85 | 84 | adantr 472 |
. . . . . 6
 
            f
   f
  cat   f
                     |
86 | 78 | fveq2d 5883 |
. . . . . . . 8
 compf  compf 
↾s           |
87 | 82 | simprd 470 |
. . . . . . . 8
 compf 
↾s         compf  cat
  f                      |
88 | 86, 87 | eqtrd 2505 |
. . . . . . 7
 compf  compf 
cat   f
                     |
89 | 88 | adantr 472 |
. . . . . 6
 
           compf  compf 
cat   f
                     |
90 | | df-br 4396 |
. . . . . . . . . . 11
    
       |
91 | | funcrcl 15846 |
. . . . . . . . . . 11
  
  
    |
92 | 90, 91 | sylbi 200 |
. . . . . . . . . 10
     
   |
93 | 92 | simpld 466 |
. . . . . . . . 9
       |
94 | | df-br 4396 |
. . . . . . . . . . 11
    
       |
95 | | funcrcl 15846 |
. . . . . . . . . . 11
  
  
    |
96 | 94, 95 | sylbi 200 |
. . . . . . . . . 10
     
   |
97 | 96 | simpld 466 |
. . . . . . . . 9
       |
98 | 93, 97 | jaoi 386 |
. . . . . . . 8
          
  |
99 | | elex 3040 |
. . . . . . . 8
   |
100 | 98, 99 | syl 17 |
. . . . . . 7
          
  |
101 | 100 | adantl 473 |
. . . . . 6
 
             |
102 | | ovex 6336 |
. . . . . . . 8
 ↾s   |
103 | 35, 102 | eqeltri 2545 |
. . . . . . 7
 |
104 | 103 | a1i 11 |
. . . . . 6
 
             |
105 | | ovex 6336 |
. . . . . . 7
 cat   f
                   |
106 | 105 | a1i 11 |
. . . . . 6
 
            cat  
f                     |
107 | 74, 75, 85, 89, 101, 101, 104, 106 | funcpropd 15883 |
. . . . 5
 
               cat  
f                      |
108 | 107 | breqd 4406 |
. . . 4
 
             
     cat   f
                       |
109 | 73, 108 | bitr4d 264 |
. . 3
 
             
         |
110 | 109 | ex 441 |
. 2
    
 
    
    
        |
111 | 2, 4, 110 | pm5.21ndd 361 |
1
     
       |