# Metamath Proof Explorer

## Theorem srhmsubc

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 special ring homomorphisms (i.e. ring homomorphisms from a special ring to another ring of that kind) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020)

Ref Expression
Hypotheses srhmsubc.s ${⊢}\forall {r}\in {S}\phantom{\rule{.4em}{0ex}}{r}\in \mathrm{Ring}$
srhmsubc.c ${⊢}{C}={U}\cap {S}$
srhmsubc.j ${⊢}{J}=\left({r}\in {C},{s}\in {C}⟼{r}\mathrm{RingHom}{s}\right)$
Assertion srhmsubc ${⊢}{U}\in {V}\to {J}\in \mathrm{Subcat}\left(\mathrm{RingCat}\left({U}\right)\right)$

### Proof

Step Hyp Ref Expression
1 srhmsubc.s ${⊢}\forall {r}\in {S}\phantom{\rule{.4em}{0ex}}{r}\in \mathrm{Ring}$
2 srhmsubc.c ${⊢}{C}={U}\cap {S}$
3 srhmsubc.j ${⊢}{J}=\left({r}\in {C},{s}\in {C}⟼{r}\mathrm{RingHom}{s}\right)$
4 eleq1w ${⊢}{r}={x}\to \left({r}\in \mathrm{Ring}↔{x}\in \mathrm{Ring}\right)$
5 4 1 vtoclri ${⊢}{x}\in {S}\to {x}\in \mathrm{Ring}$
6 5 ssriv ${⊢}{S}\subseteq \mathrm{Ring}$
7 sslin ${⊢}{S}\subseteq \mathrm{Ring}\to {U}\cap {S}\subseteq {U}\cap \mathrm{Ring}$
8 6 7 mp1i ${⊢}{U}\in {V}\to {U}\cap {S}\subseteq {U}\cap \mathrm{Ring}$
9 2 8 eqsstrid ${⊢}{U}\in {V}\to {C}\subseteq {U}\cap \mathrm{Ring}$
10 ssid ${⊢}{x}\mathrm{RingHom}{y}\subseteq {x}\mathrm{RingHom}{y}$
11 eqid ${⊢}\mathrm{RingCat}\left({U}\right)=\mathrm{RingCat}\left({U}\right)$
12 eqid ${⊢}{\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}={\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
13 simpl ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {U}\in {V}$
14 eqid ${⊢}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right)=\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right)$
15 1 2 srhmsubclem2 ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to {x}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
16 15 adantrr ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
17 1 2 srhmsubclem2 ${⊢}\left({U}\in {V}\wedge {y}\in {C}\right)\to {y}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
18 17 adantrl ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {y}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
19 11 12 13 14 16 18 ringchom ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){y}={x}\mathrm{RingHom}{y}$
20 10 19 sseqtrrid ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}\mathrm{RingHom}{y}\subseteq {x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){y}$
21 3 a1i ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {J}=\left({r}\in {C},{s}\in {C}⟼{r}\mathrm{RingHom}{s}\right)$
22 oveq12 ${⊢}\left({r}={x}\wedge {s}={y}\right)\to {r}\mathrm{RingHom}{s}={x}\mathrm{RingHom}{y}$
23 22 adantl ${⊢}\left(\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\wedge \left({r}={x}\wedge {s}={y}\right)\right)\to {r}\mathrm{RingHom}{s}={x}\mathrm{RingHom}{y}$
24 simprl ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}\in {C}$
25 simprr ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {y}\in {C}$
26 ovexd ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}\mathrm{RingHom}{y}\in \mathrm{V}$
27 21 23 24 25 26 ovmpod ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}{J}{y}={x}\mathrm{RingHom}{y}$
28 eqid ${⊢}{\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right)$
29 28 12 14 16 18 homfval ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}{\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right){y}={x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){y}$
30 20 27 29 3sstr4d ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}{J}{y}\subseteq {x}{\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right){y}$
31 30 ralrimivva ${⊢}{U}\in {V}\to \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{x}{J}{y}\subseteq {x}{\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right){y}$
32 ovex ${⊢}{r}\mathrm{RingHom}{s}\in \mathrm{V}$
33 3 32 fnmpoi ${⊢}{J}Fn\left({C}×{C}\right)$
34 33 a1i ${⊢}{U}\in {V}\to {J}Fn\left({C}×{C}\right)$
35 28 12 homffn ${⊢}{\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right)Fn\left({\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}×{\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}\right)$
36 id ${⊢}{U}\in {V}\to {U}\in {V}$
37 11 12 36 ringcbas ${⊢}{U}\in {V}\to {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}={U}\cap \mathrm{Ring}$
38 37 eqcomd ${⊢}{U}\in {V}\to {U}\cap \mathrm{Ring}={\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
39 38 sqxpeqd ${⊢}{U}\in {V}\to \left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)={\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}×{\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
40 39 fneq2d ${⊢}{U}\in {V}\to \left({\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right)Fn\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)↔{\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right)Fn\left({\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}×{\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}\right)\right)$
41 35 40 mpbiri ${⊢}{U}\in {V}\to {\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right)Fn\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)$
42 inex1g ${⊢}{U}\in {V}\to {U}\cap \mathrm{Ring}\in \mathrm{V}$
43 34 41 42 isssc ${⊢}{U}\in {V}\to \left({J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right)↔\left({C}\subseteq {U}\cap \mathrm{Ring}\wedge \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{x}{J}{y}\subseteq {x}{\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right){y}\right)\right)$
44 9 31 43 mpbir2and ${⊢}{U}\in {V}\to {J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right)$
45 2 elin2 ${⊢}{x}\in {C}↔\left({x}\in {U}\wedge {x}\in {S}\right)$
46 5 adantl ${⊢}\left({x}\in {U}\wedge {x}\in {S}\right)\to {x}\in \mathrm{Ring}$
47 45 46 sylbi ${⊢}{x}\in {C}\to {x}\in \mathrm{Ring}$
48 47 adantl ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to {x}\in \mathrm{Ring}$
49 eqid ${⊢}{\mathrm{Base}}_{{x}}={\mathrm{Base}}_{{x}}$
50 49 idrhm ${⊢}{x}\in \mathrm{Ring}\to {\mathrm{I}↾}_{{\mathrm{Base}}_{{x}}}\in \left({x}\mathrm{RingHom}{x}\right)$
51 48 50 syl ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to {\mathrm{I}↾}_{{\mathrm{Base}}_{{x}}}\in \left({x}\mathrm{RingHom}{x}\right)$
52 eqid ${⊢}\mathrm{Id}\left(\mathrm{RingCat}\left({U}\right)\right)=\mathrm{Id}\left(\mathrm{RingCat}\left({U}\right)\right)$
53 simpl ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to {U}\in {V}$
54 11 12 52 53 15 49 ringcid ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to \mathrm{Id}\left(\mathrm{RingCat}\left({U}\right)\right)\left({x}\right)={\mathrm{I}↾}_{{\mathrm{Base}}_{{x}}}$
55 3 a1i ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to {J}=\left({r}\in {C},{s}\in {C}⟼{r}\mathrm{RingHom}{s}\right)$
56 oveq12 ${⊢}\left({r}={x}\wedge {s}={x}\right)\to {r}\mathrm{RingHom}{s}={x}\mathrm{RingHom}{x}$
57 56 adantl ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({r}={x}\wedge {s}={x}\right)\right)\to {r}\mathrm{RingHom}{s}={x}\mathrm{RingHom}{x}$
58 simpr ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to {x}\in {C}$
59 ovexd ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to {x}\mathrm{RingHom}{x}\in \mathrm{V}$
60 55 57 58 58 59 ovmpod ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to {x}{J}{x}={x}\mathrm{RingHom}{x}$
61 51 54 60 3eltr4d ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to \mathrm{Id}\left(\mathrm{RingCat}\left({U}\right)\right)\left({x}\right)\in \left({x}{J}{x}\right)$
62 eqid ${⊢}\mathrm{comp}\left(\mathrm{RingCat}\left({U}\right)\right)=\mathrm{comp}\left(\mathrm{RingCat}\left({U}\right)\right)$
63 11 ringccat ${⊢}{U}\in {V}\to \mathrm{RingCat}\left({U}\right)\in \mathrm{Cat}$
64 63 ad3antrrr ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to \mathrm{RingCat}\left({U}\right)\in \mathrm{Cat}$
65 15 adantr ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {x}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
66 65 adantr ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to {x}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
67 17 ad2ant2r ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {y}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
68 67 adantr ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to {y}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
69 1 2 srhmsubclem2 ${⊢}\left({U}\in {V}\wedge {z}\in {C}\right)\to {z}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
70 69 ad2ant2rl ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {z}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
71 70 adantr ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to {z}\in {\mathrm{Base}}_{\mathrm{RingCat}\left({U}\right)}$
72 53 adantr ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {U}\in {V}$
73 simpl ${⊢}\left({y}\in {C}\wedge {z}\in {C}\right)\to {y}\in {C}$
74 58 73 anim12i ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to \left({x}\in {C}\wedge {y}\in {C}\right)$
75 72 74 jca ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to \left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)$
76 1 2 3 srhmsubclem3 ${⊢}\left({U}\in {V}\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}{J}{y}={x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){y}$
77 75 76 syl ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {x}{J}{y}={x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){y}$
78 77 eleq2d ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to \left({f}\in \left({x}{J}{y}\right)↔{f}\in \left({x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){y}\right)\right)$
79 78 biimpcd ${⊢}{f}\in \left({x}{J}{y}\right)\to \left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {f}\in \left({x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){y}\right)\right)$
80 79 adantr ${⊢}\left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\to \left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {f}\in \left({x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){y}\right)\right)$
81 80 impcom ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to {f}\in \left({x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){y}\right)$
82 1 2 3 srhmsubclem3 ${⊢}\left({U}\in {V}\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {y}{J}{z}={y}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){z}$
83 82 adantlr ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {y}{J}{z}={y}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){z}$
84 83 eleq2d ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to \left({g}\in \left({y}{J}{z}\right)↔{g}\in \left({y}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right)\right)$
85 84 biimpd ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to \left({g}\in \left({y}{J}{z}\right)\to {g}\in \left({y}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right)\right)$
86 85 adantld ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to \left(\left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\to {g}\in \left({y}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right)\right)$
87 86 imp ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to {g}\in \left({y}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right)$
88 12 14 62 64 66 68 71 81 87 catcocl ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to {g}\left(⟨{x},{y}⟩\mathrm{comp}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right){f}\in \left({x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right)$
89 11 12 72 14 65 70 ringchom ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){z}={x}\mathrm{RingHom}{z}$
90 89 eqcomd ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {x}\mathrm{RingHom}{z}={x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){z}$
91 90 adantr ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to {x}\mathrm{RingHom}{z}={x}\mathrm{Hom}\left(\mathrm{RingCat}\left({U}\right)\right){z}$
92 88 91 eleqtrrd ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to {g}\left(⟨{x},{y}⟩\mathrm{comp}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right){f}\in \left({x}\mathrm{RingHom}{z}\right)$
93 3 a1i ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {J}=\left({r}\in {C},{s}\in {C}⟼{r}\mathrm{RingHom}{s}\right)$
94 oveq12 ${⊢}\left({r}={x}\wedge {s}={z}\right)\to {r}\mathrm{RingHom}{s}={x}\mathrm{RingHom}{z}$
95 94 adantl ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({r}={x}\wedge {s}={z}\right)\right)\to {r}\mathrm{RingHom}{s}={x}\mathrm{RingHom}{z}$
96 58 adantr ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {x}\in {C}$
97 simprr ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {z}\in {C}$
98 ovexd ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {x}\mathrm{RingHom}{z}\in \mathrm{V}$
99 93 95 96 97 98 ovmpod ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to {x}{J}{z}={x}\mathrm{RingHom}{z}$
100 99 adantr ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to {x}{J}{z}={x}\mathrm{RingHom}{z}$
101 92 100 eleqtrrd ${⊢}\left(\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\wedge \left({f}\in \left({x}{J}{y}\right)\wedge {g}\in \left({y}{J}{z}\right)\right)\right)\to {g}\left(⟨{x},{y}⟩\mathrm{comp}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right){f}\in \left({x}{J}{z}\right)$
102 101 ralrimivva ${⊢}\left(\left({U}\in {V}\wedge {x}\in {C}\right)\wedge \left({y}\in {C}\wedge {z}\in {C}\right)\right)\to \forall {f}\in \left({x}{J}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{J}{z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right){f}\in \left({x}{J}{z}\right)$
103 102 ralrimivva ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{J}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{J}{z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right){f}\in \left({x}{J}{z}\right)$
104 61 103 jca ${⊢}\left({U}\in {V}\wedge {x}\in {C}\right)\to \left(\mathrm{Id}\left(\mathrm{RingCat}\left({U}\right)\right)\left({x}\right)\in \left({x}{J}{x}\right)\wedge \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{J}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{J}{z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right){f}\in \left({x}{J}{z}\right)\right)$
105 104 ralrimiva ${⊢}{U}\in {V}\to \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Id}\left(\mathrm{RingCat}\left({U}\right)\right)\left({x}\right)\in \left({x}{J}{x}\right)\wedge \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{J}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{J}{z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right){f}\in \left({x}{J}{z}\right)\right)$
106 28 52 62 63 34 issubc2 ${⊢}{U}\in {V}\to \left({J}\in \mathrm{Subcat}\left(\mathrm{RingCat}\left({U}\right)\right)↔\left({J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left(\mathrm{RingCat}\left({U}\right)\right)\wedge \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Id}\left(\mathrm{RingCat}\left({U}\right)\right)\left({x}\right)\in \left({x}{J}{x}\right)\wedge \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{J}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{J}{z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left(\mathrm{RingCat}\left({U}\right)\right){z}\right){f}\in \left({x}{J}{z}\right)\right)\right)\right)$
107 44 105 106 mpbir2and ${⊢}{U}\in {V}\to {J}\in \mathrm{Subcat}\left(\mathrm{RingCat}\left({U}\right)\right)$