Metamath Proof Explorer


Theorem resscat

Description: A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion resscat C Cat S V C 𝑠 S Cat

Proof

Step Hyp Ref Expression
1 eqid Base C = Base C
2 1 ressinbas S V C 𝑠 S = C 𝑠 S Base C
3 2 adantl C Cat S V C 𝑠 S = C 𝑠 S Base C
4 eqid C cat Hom 𝑓 C S Base C × S Base C = C cat Hom 𝑓 C S Base C × S Base C
5 eqid Hom 𝑓 C = Hom 𝑓 C
6 simpl C Cat S V C Cat
7 inss2 S Base C Base C
8 7 a1i C Cat S V S Base C Base C
9 1 5 6 8 fullsubc C Cat S V Hom 𝑓 C S Base C × S Base C Subcat C
10 4 9 subccat C Cat S V C cat Hom 𝑓 C S Base C × S Base C Cat
11 eqid C 𝑠 S Base C = C 𝑠 S Base C
12 1 5 6 8 11 4 fullresc C Cat S V Hom 𝑓 C 𝑠 S Base C = Hom 𝑓 C cat Hom 𝑓 C S Base C × S Base C comp 𝑓 C 𝑠 S Base C = comp 𝑓 C cat Hom 𝑓 C S Base C × S Base C
13 12 simpld C Cat S V Hom 𝑓 C 𝑠 S Base C = Hom 𝑓 C cat Hom 𝑓 C S Base C × S Base C
14 12 simprd C Cat S V comp 𝑓 C 𝑠 S Base C = comp 𝑓 C cat Hom 𝑓 C S Base C × S Base C
15 ovexd C Cat S V C 𝑠 S Base C V
16 13 14 15 10 catpropd C Cat S V C 𝑠 S Base C Cat C cat Hom 𝑓 C S Base C × S Base C Cat
17 10 16 mpbird C Cat S V C 𝑠 S Base C Cat
18 3 17 eqeltrd C Cat S V C 𝑠 S Cat