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=BaseC
fullsubc.h H=Hom𝑓C
fullsubc.c φCCat
fullsubc.s φSB
Assertion fullsubc φHS×SSubcatC

Proof

Step Hyp Ref Expression
1 fullsubc.b B=BaseC
2 fullsubc.h H=Hom𝑓C
3 fullsubc.c φCCat
4 fullsubc.s φSB
5 2 1 homffn HFnB×B
6 1 fvexi BV
7 sscres HFnB×BBVHS×ScatH
8 5 6 7 mp2an HS×ScatH
9 8 a1i φHS×ScatH
10 eqid HomC=HomC
11 eqid IdC=IdC
12 3 adantr φxSCCat
13 4 sselda φxSxB
14 1 10 11 12 13 catidcl φxSIdCxxHomCx
15 simpr φxSxS
16 15 15 ovresd φxSxHS×Sx=xHx
17 2 1 10 13 13 homfval φxSxHx=xHomCx
18 16 17 eqtrd φxSxHS×Sx=xHomCx
19 14 18 eleqtrrd φxSIdCxxHS×Sx
20 eqid compC=compC
21 12 ad3antrrr φxSySzSfxHomCygyHomCzCCat
22 13 ad3antrrr φxSySzSfxHomCygyHomCzxB
23 4 adantr φxSSB
24 23 sselda φxSySyB
25 24 adantr φxSySzSyB
26 25 adantr φxSySzSfxHomCygyHomCzyB
27 23 adantr φxSySSB
28 27 sselda φxSySzSzB
29 28 adantr φxSySzSfxHomCygyHomCzzB
30 simprl φxSySzSfxHomCygyHomCzfxHomCy
31 simprr φxSySzSfxHomCygyHomCzgyHomCz
32 1 10 20 21 22 26 29 30 31 catcocl φxSySzSfxHomCygyHomCzgxycompCzfxHomCz
33 15 ad3antrrr φxSySzSfxHomCygyHomCzxS
34 simplr φxSySzSfxHomCygyHomCzzS
35 33 34 ovresd φxSySzSfxHomCygyHomCzxHS×Sz=xHz
36 2 1 10 22 29 homfval φxSySzSfxHomCygyHomCzxHz=xHomCz
37 35 36 eqtrd φxSySzSfxHomCygyHomCzxHS×Sz=xHomCz
38 32 37 eleqtrrd φxSySzSfxHomCygyHomCzgxycompCzfxHS×Sz
39 38 ralrimivva φxSySzSfxHomCygyHomCzgxycompCzfxHS×Sz
40 simplr φxSySxS
41 simpr φxSySyS
42 40 41 ovresd φxSySxHS×Sy=xHy
43 13 adantr φxSySxB
44 2 1 10 43 24 homfval φxSySxHy=xHomCy
45 42 44 eqtrd φxSySxHS×Sy=xHomCy
46 45 adantr φxSySzSxHS×Sy=xHomCy
47 simplr φxSySzSyS
48 simpr φxSySzSzS
49 47 48 ovresd φxSySzSyHS×Sz=yHz
50 2 1 10 25 28 homfval φxSySzSyHz=yHomCz
51 49 50 eqtrd φxSySzSyHS×Sz=yHomCz
52 51 raleqdv φxSySzSgyHS×SzgxycompCzfxHS×SzgyHomCzgxycompCzfxHS×Sz
53 46 52 raleqbidv φxSySzSfxHS×SygyHS×SzgxycompCzfxHS×SzfxHomCygyHomCzgxycompCzfxHS×Sz
54 39 53 mpbird φxSySzSfxHS×SygyHS×SzgxycompCzfxHS×Sz
55 54 ralrimiva φxSySzSfxHS×SygyHS×SzgxycompCzfxHS×Sz
56 55 ralrimiva φxSySzSfxHS×SygyHS×SzgxycompCzfxHS×Sz
57 19 56 jca φxSIdCxxHS×SxySzSfxHS×SygyHS×SzgxycompCzfxHS×Sz
58 57 ralrimiva φxSIdCxxHS×SxySzSfxHS×SygyHS×SzgxycompCzfxHS×Sz
59 xpss12 SBSBS×SB×B
60 4 4 59 syl2anc φS×SB×B
61 fnssres HFnB×BS×SB×BHS×SFnS×S
62 5 60 61 sylancr φHS×SFnS×S
63 2 11 20 3 62 issubc2 φHS×SSubcatCHS×ScatHxSIdCxxHS×SxySzSfxHS×SygyHS×SzgxycompCzfxHS×Sz
64 9 58 63 mpbir2and φHS×SSubcatC