Description: According to df-subc , the subcategories ( SubcatC ) of a category C are subsets of the homomorphisms of C (see subcssc and subcss2 ). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rngcrescrhm.u | |
|
rngcrescrhm.c | |
||
rngcrescrhm.r | |
||
rngcrescrhm.h | |
||
Assertion | rhmsubc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rngcrescrhm.u | |
|
2 | rngcrescrhm.c | |
|
3 | rngcrescrhm.r | |
|
4 | rngcrescrhm.h | |
|
5 | eqidd | |
|
6 | 1 3 5 | rhmsscrnghm | |
7 | 4 | a1i | |
8 | 2 | a1i | |
9 | 8 | eqcomd | |
10 | 9 | fveq2d | |
11 | eqid | |
|
12 | 2 11 1 | rngchomfeqhom | |
13 | eqid | |
|
14 | 2 11 1 13 | rngchomfval | |
15 | 2 11 1 | rngcbas | |
16 | incom | |
|
17 | 15 16 | eqtrdi | |
18 | 17 | sqxpeqd | |
19 | 18 | reseq2d | |
20 | 14 19 | eqtrd | |
21 | 10 12 20 | 3eqtrd | |
22 | 6 7 21 | 3brtr4d | |
23 | 1 2 3 4 | rhmsubclem3 | |
24 | 1 2 3 4 | rhmsubclem4 | |
25 | 24 | ralrimivva | |
26 | 25 | ralrimivva | |
27 | 23 26 | jca | |
28 | 27 | ralrimiva | |
29 | eqid | |
|
30 | eqid | |
|
31 | eqid | |
|
32 | eqid | |
|
33 | 32 | rngccat | |
34 | 1 33 | syl | |
35 | 1 2 3 4 | rhmsubclem1 | |
36 | 29 30 31 34 35 | issubc2 | |
37 | 22 28 36 | mpbir2and | |