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 ‘ 𝑈 ) ) )