This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring
srhmsubc.c ⊢ 𝐶 = ( 𝑈 ∩ 𝑆 )
srhmsubc.j ⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion srhmsubc ( 𝑈 ∈ 𝑉 → 𝐽 ∈ ( Subcat ‘ ( RingCat ‘ 𝑈 ) ) )

Proof

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