Description: A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subccat.1 | |
|
subccat.j | |
||
subccatid.1 | |
||
subccatid.2 | |
||
Assertion | subccatid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subccat.1 | |
|
2 | subccat.j | |
|
3 | subccatid.1 | |
|
4 | subccatid.2 | |
|
5 | eqid | |
|
6 | subcrcl | |
|
7 | 2 6 | syl | |
8 | 2 3 5 | subcss1 | |
9 | 1 5 7 3 8 | rescbas | |
10 | 1 5 7 3 8 | reschom | |
11 | eqid | |
|
12 | 1 5 7 3 8 11 | rescco | |
13 | 1 | ovexi | |
14 | 13 | a1i | |
15 | biid | |
|
16 | 2 | adantr | |
17 | 3 | adantr | |
18 | simpr | |
|
19 | 16 17 18 4 | subcidcl | |
20 | eqid | |
|
21 | 7 | adantr | |
22 | 8 | adantr | |
23 | simpr1l | |
|
24 | 22 23 | sseldd | |
25 | simpr1r | |
|
26 | 22 25 | sseldd | |
27 | 2 | adantr | |
28 | 3 | adantr | |
29 | 27 28 20 23 25 | subcss2 | |
30 | simpr31 | |
|
31 | 29 30 | sseldd | |
32 | 5 20 4 21 24 11 26 31 | catlid | |
33 | simpr2l | |
|
34 | 22 33 | sseldd | |
35 | 27 28 20 25 33 | subcss2 | |
36 | simpr32 | |
|
37 | 35 36 | sseldd | |
38 | 5 20 4 21 26 11 34 37 | catrid | |
39 | 27 28 23 11 25 33 30 36 | subccocl | |
40 | simpr2r | |
|
41 | 22 40 | sseldd | |
42 | 27 28 20 33 40 | subcss2 | |
43 | simpr33 | |
|
44 | 42 43 | sseldd | |
45 | 5 20 11 21 24 26 34 31 37 41 44 | catass | |
46 | 9 10 12 14 15 19 32 38 39 45 | iscatd2 | |