Description: A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subcidcl.j | |
|
subcidcl.2 | |
||
subcidcl.x | |
||
subccocl.o | |
||
subccocl.y | |
||
subccocl.z | |
||
subccocl.f | |
||
subccocl.g | |
||
Assertion | subccocl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subcidcl.j | |
|
2 | subcidcl.2 | |
|
3 | subcidcl.x | |
|
4 | subccocl.o | |
|
5 | subccocl.y | |
|
6 | subccocl.z | |
|
7 | subccocl.f | |
|
8 | subccocl.g | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | subcrcl | |
|
12 | 1 11 | syl | |
13 | 9 10 4 12 2 | issubc2 | |
14 | 1 13 | mpbid | |
15 | 14 | simprd | |
16 | 5 | adantr | |
17 | 6 | ad2antrr | |
18 | 7 | ad3antrrr | |
19 | simpllr | |
|
20 | simplr | |
|
21 | 19 20 | oveq12d | |
22 | 18 21 | eleqtrrd | |
23 | 8 | ad4antr | |
24 | simpllr | |
|
25 | simplr | |
|
26 | 24 25 | oveq12d | |
27 | 23 26 | eleqtrrd | |
28 | simp-5r | |
|
29 | simp-4r | |
|
30 | 28 29 | opeq12d | |
31 | simpllr | |
|
32 | 30 31 | oveq12d | |
33 | simpr | |
|
34 | simplr | |
|
35 | 32 33 34 | oveq123d | |
36 | 28 31 | oveq12d | |
37 | 35 36 | eleq12d | |
38 | 27 37 | rspcdv | |
39 | 22 38 | rspcimdv | |
40 | 17 39 | rspcimdv | |
41 | 16 40 | rspcimdv | |
42 | 41 | adantld | |
43 | 3 42 | rspcimdv | |
44 | 15 43 | mpd | |