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 | |
|
fullsubc.h | |
||
fullsubc.c | |
||
fullsubc.s | |
||
Assertion | fullsubc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fullsubc.b | |
|
2 | fullsubc.h | |
|
3 | fullsubc.c | |
|
4 | fullsubc.s | |
|
5 | 2 1 | homffn | |
6 | 1 | fvexi | |
7 | sscres | |
|
8 | 5 6 7 | mp2an | |
9 | 8 | a1i | |
10 | eqid | |
|
11 | eqid | |
|
12 | 3 | adantr | |
13 | 4 | sselda | |
14 | 1 10 11 12 13 | catidcl | |
15 | simpr | |
|
16 | 15 15 | ovresd | |
17 | 2 1 10 13 13 | homfval | |
18 | 16 17 | eqtrd | |
19 | 14 18 | eleqtrrd | |
20 | eqid | |
|
21 | 12 | ad3antrrr | |
22 | 13 | ad3antrrr | |
23 | 4 | adantr | |
24 | 23 | sselda | |
25 | 24 | adantr | |
26 | 25 | adantr | |
27 | 23 | adantr | |
28 | 27 | sselda | |
29 | 28 | adantr | |
30 | simprl | |
|
31 | simprr | |
|
32 | 1 10 20 21 22 26 29 30 31 | catcocl | |
33 | 15 | ad3antrrr | |
34 | simplr | |
|
35 | 33 34 | ovresd | |
36 | 2 1 10 22 29 | homfval | |
37 | 35 36 | eqtrd | |
38 | 32 37 | eleqtrrd | |
39 | 38 | ralrimivva | |
40 | simplr | |
|
41 | simpr | |
|
42 | 40 41 | ovresd | |
43 | 13 | adantr | |
44 | 2 1 10 43 24 | homfval | |
45 | 42 44 | eqtrd | |
46 | 45 | adantr | |
47 | simplr | |
|
48 | simpr | |
|
49 | 47 48 | ovresd | |
50 | 2 1 10 25 28 | homfval | |
51 | 49 50 | eqtrd | |
52 | 51 | raleqdv | |
53 | 46 52 | raleqbidv | |
54 | 39 53 | mpbird | |
55 | 54 | ralrimiva | |
56 | 55 | ralrimiva | |
57 | 19 56 | jca | |
58 | 57 | ralrimiva | |
59 | xpss12 | |
|
60 | 4 4 59 | syl2anc | |
61 | fnssres | |
|
62 | 5 60 61 | sylancr | |
63 | 2 11 20 3 62 | issubc2 | |
64 | 9 58 63 | mpbir2and | |