Metamath Proof Explorer


Theorem fullsubc

Description: The full subcategory generated by a subset of objects is the category with these objects and the same morphisms as the original. The result is always a subcategory (and it is full, meaning that all morphisms of the original category between objects in the subcategory is also in the subcategory), see definition 4.1(2) of Adamek p. 48. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses fullsubc.b B = Base C
fullsubc.h H = Hom 𝑓 C
fullsubc.c φ C Cat
fullsubc.s φ S B
Assertion fullsubc φ H S × S Subcat C

Proof

Step Hyp Ref Expression
1 fullsubc.b B = Base C
2 fullsubc.h H = Hom 𝑓 C
3 fullsubc.c φ C Cat
4 fullsubc.s φ S B
5 2 1 homffn H Fn B × B
6 1 fvexi B V
7 sscres H Fn B × B B V H S × S cat H
8 5 6 7 mp2an H S × S cat H
9 8 a1i φ H S × S cat H
10 eqid Hom C = Hom C
11 eqid Id C = Id C
12 3 adantr φ x S C Cat
13 4 sselda φ x S x B
14 1 10 11 12 13 catidcl φ x S Id C x x Hom C x
15 simpr φ x S x S
16 15 15 ovresd φ x S x H S × S x = x H x
17 2 1 10 13 13 homfval φ x S x H x = x Hom C x
18 16 17 eqtrd φ x S x H S × S x = x Hom C x
19 14 18 eleqtrrd φ x S Id C x x H S × S x
20 eqid comp C = comp C
21 12 ad3antrrr φ x S y S z S f x Hom C y g y Hom C z C Cat
22 13 ad3antrrr φ x S y S z S f x Hom C y g y Hom C z x B
23 4 adantr φ x S S B
24 23 sselda φ x S y S y B
25 24 adantr φ x S y S z S y B
26 25 adantr φ x S y S z S f x Hom C y g y Hom C z y B
27 23 adantr φ x S y S S B
28 27 sselda φ x S y S z S z B
29 28 adantr φ x S y S z S f x Hom C y g y Hom C z z B
30 simprl φ x S y S z S f x Hom C y g y Hom C z f x Hom C y
31 simprr φ x S y S z S f x Hom C y g y Hom C z g y Hom C z
32 1 10 20 21 22 26 29 30 31 catcocl φ x S y S z S f x Hom C y g y Hom C z g x y comp C z f x Hom C z
33 15 ad3antrrr φ x S y S z S f x Hom C y g y Hom C z x S
34 simplr φ x S y S z S f x Hom C y g y Hom C z z S
35 33 34 ovresd φ x S y S z S f x Hom C y g y Hom C z x H S × S z = x H z
36 2 1 10 22 29 homfval φ x S y S z S f x Hom C y g y Hom C z x H z = x Hom C z
37 35 36 eqtrd φ x S y S z S f x Hom C y g y Hom C z x H S × S z = x Hom C z
38 32 37 eleqtrrd φ x S y S z S f x Hom C y g y Hom C z g x y comp C z f x H S × S z
39 38 ralrimivva φ x S y S z S f x Hom C y g y Hom C z g x y comp C z f x H S × S z
40 simplr φ x S y S x S
41 simpr φ x S y S y S
42 40 41 ovresd φ x S y S x H S × S y = x H y
43 13 adantr φ x S y S x B
44 2 1 10 43 24 homfval φ x S y S x H y = x Hom C y
45 42 44 eqtrd φ x S y S x H S × S y = x Hom C y
46 45 adantr φ x S y S z S x H S × S y = x Hom C y
47 simplr φ x S y S z S y S
48 simpr φ x S y S z S z S
49 47 48 ovresd φ x S y S z S y H S × S z = y H z
50 2 1 10 25 28 homfval φ x S y S z S y H z = y Hom C z
51 49 50 eqtrd φ x S y S z S y H S × S z = y Hom C z
52 51 raleqdv φ x S y S z S g y H S × S z g x y comp C z f x H S × S z g y Hom C z g x y comp C z f x H S × S z
53 46 52 raleqbidv φ x S y S z S f x H S × S y g y H S × S z g x y comp C z f x H S × S z f x Hom C y g y Hom C z g x y comp C z f x H S × S z
54 39 53 mpbird φ x S y S z S f x H S × S y g y H S × S z g x y comp C z f x H S × S z
55 54 ralrimiva φ x S y S z S f x H S × S y g y H S × S z g x y comp C z f x H S × S z
56 55 ralrimiva φ x S y S z S f x H S × S y g y H S × S z g x y comp C z f x H S × S z
57 19 56 jca φ x S Id C x x H S × S x y S z S f x H S × S y g y H S × S z g x y comp C z f x H S × S z
58 57 ralrimiva φ x S Id C x x H S × S x y S z S f x H S × S y g y H S × S z g x y comp C z f x H S × S z
59 xpss12 S B S B S × S B × B
60 4 4 59 syl2anc φ S × S B × B
61 fnssres H Fn B × B S × S B × B H S × S Fn S × S
62 5 60 61 sylancr φ H S × S Fn S × S
63 2 11 20 3 62 issubc2 φ H S × S Subcat C H S × S cat H x S Id C x x H S × S x y S z S f x H S × S y g y H S × S z g x y comp C z f x H S × S z
64 9 58 63 mpbir2and φ H S × S Subcat C