Description: The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rngcrescrhm.u | |
|
rngcrescrhm.c | |
||
rngcrescrhm.r | |
||
rngcrescrhm.h | |
||
Assertion | rngcrescrhm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rngcrescrhm.u | |
|
2 | rngcrescrhm.c | |
|
3 | rngcrescrhm.r | |
|
4 | rngcrescrhm.h | |
|
5 | eqid | |
|
6 | 2 | fvexi | |
7 | 6 | a1i | |
8 | incom | |
|
9 | 3 8 | eqtrdi | |
10 | inex1g | |
|
11 | 1 10 | syl | |
12 | 9 11 | eqeltrd | |
13 | inss1 | |
|
14 | 3 13 | eqsstrdi | |
15 | xpss12 | |
|
16 | 14 14 15 | syl2anc | |
17 | rhmfn | |
|
18 | fnssresb | |
|
19 | 17 18 | mp1i | |
20 | 16 19 | mpbird | |
21 | 4 | fneq1i | |
22 | 20 21 | sylibr | |
23 | 5 7 12 22 | rescval2 | |