Metamath Proof Explorer


Theorem resssetc

Description: The restriction of the category of sets to a subset is the category of sets in the subset. Thus, the SetCatU categories for different U are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses resssetc.c C = SetCat U
resssetc.d D = SetCat V
resssetc.1 φ U W
resssetc.2 φ V U
Assertion resssetc φ Hom 𝑓 C 𝑠 V = Hom 𝑓 D comp 𝑓 C 𝑠 V = comp 𝑓 D

Proof

Step Hyp Ref Expression
1 resssetc.c C = SetCat U
2 resssetc.d D = SetCat V
3 resssetc.1 φ U W
4 resssetc.2 φ V U
5 3 4 ssexd φ V V
6 5 adantr φ x V y V V V
7 eqid Hom D = Hom D
8 simprl φ x V y V x V
9 simprr φ x V y V y V
10 2 6 7 8 9 setchom φ x V y V x Hom D y = y x
11 3 adantr φ x V y V U W
12 eqid Hom C = Hom C
13 4 adantr φ x V y V V U
14 13 8 sseldd φ x V y V x U
15 13 9 sseldd φ x V y V y U
16 1 11 12 14 15 setchom φ x V y V x Hom C y = y x
17 eqid C 𝑠 V = C 𝑠 V
18 17 12 resshom V V Hom C = Hom C 𝑠 V
19 5 18 syl φ Hom C = Hom C 𝑠 V
20 19 oveqdr φ x V y V x Hom C y = x Hom C 𝑠 V y
21 10 16 20 3eqtr2rd φ x V y V x Hom C 𝑠 V y = x Hom D y
22 21 ralrimivva φ x V y V x Hom C 𝑠 V y = x Hom D y
23 eqid Hom C 𝑠 V = Hom C 𝑠 V
24 1 3 setcbas φ U = Base C
25 4 24 sseqtrd φ V Base C
26 eqid Base C = Base C
27 17 26 ressbas2 V Base C V = Base C 𝑠 V
28 25 27 syl φ V = Base C 𝑠 V
29 2 5 setcbas φ V = Base D
30 23 7 28 29 homfeq φ Hom 𝑓 C 𝑠 V = Hom 𝑓 D x V y V x Hom C 𝑠 V y = x Hom D y
31 22 30 mpbird φ Hom 𝑓 C 𝑠 V = Hom 𝑓 D
32 5 ad2antrr φ x V y V z V f x Hom D y g y Hom D z V V
33 eqid comp D = comp D
34 simplr1 φ x V y V z V f x Hom D y g y Hom D z x V
35 simplr2 φ x V y V z V f x Hom D y g y Hom D z y V
36 simplr3 φ x V y V z V f x Hom D y g y Hom D z z V
37 simprl φ x V y V z V f x Hom D y g y Hom D z f x Hom D y
38 2 32 7 34 35 elsetchom φ x V y V z V f x Hom D y g y Hom D z f x Hom D y f : x y
39 37 38 mpbid φ x V y V z V f x Hom D y g y Hom D z f : x y
40 simprr φ x V y V z V f x Hom D y g y Hom D z g y Hom D z
41 2 32 7 35 36 elsetchom φ x V y V z V f x Hom D y g y Hom D z g y Hom D z g : y z
42 40 41 mpbid φ x V y V z V f x Hom D y g y Hom D z g : y z
43 2 32 33 34 35 36 39 42 setcco φ x V y V z V f x Hom D y g y Hom D z g x y comp D z f = g f
44 3 ad2antrr φ x V y V z V f x Hom D y g y Hom D z U W
45 eqid comp C = comp C
46 4 ad2antrr φ x V y V z V f x Hom D y g y Hom D z V U
47 46 34 sseldd φ x V y V z V f x Hom D y g y Hom D z x U
48 46 35 sseldd φ x V y V z V f x Hom D y g y Hom D z y U
49 46 36 sseldd φ x V y V z V f x Hom D y g y Hom D z z U
50 1 44 45 47 48 49 39 42 setcco φ x V y V z V f x Hom D y g y Hom D z g x y comp C z f = g f
51 17 45 ressco V V comp C = comp C 𝑠 V
52 5 51 syl φ comp C = comp C 𝑠 V
53 52 ad2antrr φ x V y V z V f x Hom D y g y Hom D z comp C = comp C 𝑠 V
54 53 oveqd φ x V y V z V f x Hom D y g y Hom D z x y comp C z = x y comp C 𝑠 V z
55 54 oveqd φ x V y V z V f x Hom D y g y Hom D z g x y comp C z f = g x y comp C 𝑠 V z f
56 43 50 55 3eqtr2d φ x V y V z V f x Hom D y g y Hom D z g x y comp D z f = g x y comp C 𝑠 V z f
57 56 ralrimivva φ x V y V z V f x Hom D y g y Hom D z g x y comp D z f = g x y comp C 𝑠 V z f
58 57 ralrimivvva φ x V y V z V f x Hom D y g y Hom D z g x y comp D z f = g x y comp C 𝑠 V z f
59 eqid comp C 𝑠 V = comp C 𝑠 V
60 31 eqcomd φ Hom 𝑓 D = Hom 𝑓 C 𝑠 V
61 33 59 7 29 28 60 comfeq φ comp 𝑓 D = comp 𝑓 C 𝑠 V x V y V z V f x Hom D y g y Hom D z g x y comp D z f = g x y comp C 𝑠 V z f
62 58 61 mpbird φ comp 𝑓 D = comp 𝑓 C 𝑠 V
63 62 eqcomd φ comp 𝑓 C 𝑠 V = comp 𝑓 D
64 31 63 jca φ Hom 𝑓 C 𝑠 V = Hom 𝑓 D comp 𝑓 C 𝑠 V = comp 𝑓 D