MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  srhmsubc Structured version   Visualization version   GIF version

Theorem srhmsubc 20627
Description: According to df-subc 17804, the subcategories (Subcatβ€˜πΆ) of a category 𝐢 are subsets of the homomorphisms of 𝐢 (see subcssc 17835 and subcss2 17838). 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.)
Hypotheses
Ref Expression
srhmsubc.s βˆ€π‘Ÿ ∈ 𝑆 π‘Ÿ ∈ Ring
srhmsubc.c 𝐢 = (π‘ˆ ∩ 𝑆)
srhmsubc.j 𝐽 = (π‘Ÿ ∈ 𝐢, 𝑠 ∈ 𝐢 ↦ (π‘Ÿ RingHom 𝑠))
Assertion
Ref Expression
srhmsubc (π‘ˆ ∈ 𝑉 β†’ 𝐽 ∈ (Subcatβ€˜(RingCatβ€˜π‘ˆ)))
Distinct variable groups:   𝑆,π‘Ÿ   𝐢,π‘Ÿ,𝑠   π‘ˆ,π‘Ÿ,𝑠   𝑉,π‘Ÿ,𝑠
Allowed substitution hints:   𝑆(𝑠)   𝐽(𝑠,π‘Ÿ)

Proof of Theorem srhmsubc
Dummy variables 𝑓 𝑔 π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 srhmsubc.c . . . 4 𝐢 = (π‘ˆ ∩ 𝑆)
2 eleq1w 2812 . . . . . . 7 (π‘Ÿ = π‘₯ β†’ (π‘Ÿ ∈ Ring ↔ π‘₯ ∈ Ring))
3 srhmsubc.s . . . . . . 7 βˆ€π‘Ÿ ∈ 𝑆 π‘Ÿ ∈ Ring
42, 3vtoclri 3575 . . . . . 6 (π‘₯ ∈ 𝑆 β†’ π‘₯ ∈ Ring)
54ssriv 3986 . . . . 5 𝑆 βŠ† Ring
6 sslin 4237 . . . . 5 (𝑆 βŠ† Ring β†’ (π‘ˆ ∩ 𝑆) βŠ† (π‘ˆ ∩ Ring))
75, 6mp1i 13 . . . 4 (π‘ˆ ∈ 𝑉 β†’ (π‘ˆ ∩ 𝑆) βŠ† (π‘ˆ ∩ Ring))
81, 7eqsstrid 4030 . . 3 (π‘ˆ ∈ 𝑉 β†’ 𝐢 βŠ† (π‘ˆ ∩ Ring))
9 ssid 4004 . . . . . 6 (π‘₯ RingHom 𝑦) βŠ† (π‘₯ RingHom 𝑦)
10 eqid 2728 . . . . . . 7 (RingCatβ€˜π‘ˆ) = (RingCatβ€˜π‘ˆ)
11 eqid 2728 . . . . . . 7 (Baseβ€˜(RingCatβ€˜π‘ˆ)) = (Baseβ€˜(RingCatβ€˜π‘ˆ))
12 simpl 481 . . . . . . 7 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ π‘ˆ ∈ 𝑉)
13 eqid 2728 . . . . . . 7 (Hom β€˜(RingCatβ€˜π‘ˆ)) = (Hom β€˜(RingCatβ€˜π‘ˆ))
143, 1srhmsubclem2 20625 . . . . . . . 8 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
1514adantrr 715 . . . . . . 7 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ π‘₯ ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
163, 1srhmsubclem2 20625 . . . . . . . 8 ((π‘ˆ ∈ 𝑉 ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
1716adantrl 714 . . . . . . 7 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ 𝑦 ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
1810, 11, 12, 13, 15, 17ringchom 20599 . . . . . 6 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑦) = (π‘₯ RingHom 𝑦))
199, 18sseqtrrid 4035 . . . . 5 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯ RingHom 𝑦) βŠ† (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑦))
20 srhmsubc.j . . . . . . 7 𝐽 = (π‘Ÿ ∈ 𝐢, 𝑠 ∈ 𝐢 ↦ (π‘Ÿ RingHom 𝑠))
2120a1i 11 . . . . . 6 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ 𝐽 = (π‘Ÿ ∈ 𝐢, 𝑠 ∈ 𝐢 ↦ (π‘Ÿ RingHom 𝑠)))
22 oveq12 7435 . . . . . . 7 ((π‘Ÿ = π‘₯ ∧ 𝑠 = 𝑦) β†’ (π‘Ÿ RingHom 𝑠) = (π‘₯ RingHom 𝑦))
2322adantl 480 . . . . . 6 (((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) ∧ (π‘Ÿ = π‘₯ ∧ 𝑠 = 𝑦)) β†’ (π‘Ÿ RingHom 𝑠) = (π‘₯ RingHom 𝑦))
24 simprl 769 . . . . . 6 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ π‘₯ ∈ 𝐢)
25 simprr 771 . . . . . 6 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ 𝑦 ∈ 𝐢)
26 ovexd 7461 . . . . . 6 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯ RingHom 𝑦) ∈ V)
2721, 23, 24, 25, 26ovmpod 7580 . . . . 5 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯𝐽𝑦) = (π‘₯ RingHom 𝑦))
28 eqid 2728 . . . . . 6 (Homf β€˜(RingCatβ€˜π‘ˆ)) = (Homf β€˜(RingCatβ€˜π‘ˆ))
2928, 11, 13, 15, 17homfval 17681 . . . . 5 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯(Homf β€˜(RingCatβ€˜π‘ˆ))𝑦) = (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑦))
3019, 27, 293sstr4d 4029 . . . 4 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯𝐽𝑦) βŠ† (π‘₯(Homf β€˜(RingCatβ€˜π‘ˆ))𝑦))
3130ralrimivva 3198 . . 3 (π‘ˆ ∈ 𝑉 β†’ βˆ€π‘₯ ∈ 𝐢 βˆ€π‘¦ ∈ 𝐢 (π‘₯𝐽𝑦) βŠ† (π‘₯(Homf β€˜(RingCatβ€˜π‘ˆ))𝑦))
32 ovex 7459 . . . . . 6 (π‘Ÿ RingHom 𝑠) ∈ V
3320, 32fnmpoi 8082 . . . . 5 𝐽 Fn (𝐢 Γ— 𝐢)
3433a1i 11 . . . 4 (π‘ˆ ∈ 𝑉 β†’ 𝐽 Fn (𝐢 Γ— 𝐢))
3528, 11homffn 17682 . . . . 5 (Homf β€˜(RingCatβ€˜π‘ˆ)) Fn ((Baseβ€˜(RingCatβ€˜π‘ˆ)) Γ— (Baseβ€˜(RingCatβ€˜π‘ˆ)))
36 id 22 . . . . . . . . 9 (π‘ˆ ∈ 𝑉 β†’ π‘ˆ ∈ 𝑉)
3710, 11, 36ringcbas 20597 . . . . . . . 8 (π‘ˆ ∈ 𝑉 β†’ (Baseβ€˜(RingCatβ€˜π‘ˆ)) = (π‘ˆ ∩ Ring))
3837eqcomd 2734 . . . . . . 7 (π‘ˆ ∈ 𝑉 β†’ (π‘ˆ ∩ Ring) = (Baseβ€˜(RingCatβ€˜π‘ˆ)))
3938sqxpeqd 5714 . . . . . 6 (π‘ˆ ∈ 𝑉 β†’ ((π‘ˆ ∩ Ring) Γ— (π‘ˆ ∩ Ring)) = ((Baseβ€˜(RingCatβ€˜π‘ˆ)) Γ— (Baseβ€˜(RingCatβ€˜π‘ˆ))))
4039fneq2d 6653 . . . . 5 (π‘ˆ ∈ 𝑉 β†’ ((Homf β€˜(RingCatβ€˜π‘ˆ)) Fn ((π‘ˆ ∩ Ring) Γ— (π‘ˆ ∩ Ring)) ↔ (Homf β€˜(RingCatβ€˜π‘ˆ)) Fn ((Baseβ€˜(RingCatβ€˜π‘ˆ)) Γ— (Baseβ€˜(RingCatβ€˜π‘ˆ)))))
4135, 40mpbiri 257 . . . 4 (π‘ˆ ∈ 𝑉 β†’ (Homf β€˜(RingCatβ€˜π‘ˆ)) Fn ((π‘ˆ ∩ Ring) Γ— (π‘ˆ ∩ Ring)))
42 inex1g 5323 . . . 4 (π‘ˆ ∈ 𝑉 β†’ (π‘ˆ ∩ Ring) ∈ V)
4334, 41, 42isssc 17812 . . 3 (π‘ˆ ∈ 𝑉 β†’ (𝐽 βŠ†cat (Homf β€˜(RingCatβ€˜π‘ˆ)) ↔ (𝐢 βŠ† (π‘ˆ ∩ Ring) ∧ βˆ€π‘₯ ∈ 𝐢 βˆ€π‘¦ ∈ 𝐢 (π‘₯𝐽𝑦) βŠ† (π‘₯(Homf β€˜(RingCatβ€˜π‘ˆ))𝑦))))
448, 31, 43mpbir2and 711 . 2 (π‘ˆ ∈ 𝑉 β†’ 𝐽 βŠ†cat (Homf β€˜(RingCatβ€˜π‘ˆ)))
451elin2 4199 . . . . . . . 8 (π‘₯ ∈ 𝐢 ↔ (π‘₯ ∈ π‘ˆ ∧ π‘₯ ∈ 𝑆))
464adantl 480 . . . . . . . 8 ((π‘₯ ∈ π‘ˆ ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ ∈ Ring)
4745, 46sylbi 216 . . . . . . 7 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ Ring)
4847adantl 480 . . . . . 6 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ Ring)
49 eqid 2728 . . . . . . 7 (Baseβ€˜π‘₯) = (Baseβ€˜π‘₯)
5049idrhm 20443 . . . . . 6 (π‘₯ ∈ Ring β†’ ( I β†Ύ (Baseβ€˜π‘₯)) ∈ (π‘₯ RingHom π‘₯))
5148, 50syl 17 . . . . 5 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ ( I β†Ύ (Baseβ€˜π‘₯)) ∈ (π‘₯ RingHom π‘₯))
52 eqid 2728 . . . . . 6 (Idβ€˜(RingCatβ€˜π‘ˆ)) = (Idβ€˜(RingCatβ€˜π‘ˆ))
53 simpl 481 . . . . . 6 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ π‘ˆ ∈ 𝑉)
5410, 11, 52, 53, 14, 49ringcid 20611 . . . . 5 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ ((Idβ€˜(RingCatβ€˜π‘ˆ))β€˜π‘₯) = ( I β†Ύ (Baseβ€˜π‘₯)))
5520a1i 11 . . . . . 6 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ 𝐽 = (π‘Ÿ ∈ 𝐢, 𝑠 ∈ 𝐢 ↦ (π‘Ÿ RingHom 𝑠)))
56 oveq12 7435 . . . . . . 7 ((π‘Ÿ = π‘₯ ∧ 𝑠 = π‘₯) β†’ (π‘Ÿ RingHom 𝑠) = (π‘₯ RingHom π‘₯))
5756adantl 480 . . . . . 6 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (π‘Ÿ = π‘₯ ∧ 𝑠 = π‘₯)) β†’ (π‘Ÿ RingHom 𝑠) = (π‘₯ RingHom π‘₯))
58 simpr 483 . . . . . 6 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ 𝐢)
59 ovexd 7461 . . . . . 6 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ (π‘₯ RingHom π‘₯) ∈ V)
6055, 57, 58, 58, 59ovmpod 7580 . . . . 5 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ (π‘₯𝐽π‘₯) = (π‘₯ RingHom π‘₯))
6151, 54, 603eltr4d 2844 . . . 4 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ ((Idβ€˜(RingCatβ€˜π‘ˆ))β€˜π‘₯) ∈ (π‘₯𝐽π‘₯))
62 eqid 2728 . . . . . . . . 9 (compβ€˜(RingCatβ€˜π‘ˆ)) = (compβ€˜(RingCatβ€˜π‘ˆ))
6310ringccat 20610 . . . . . . . . . 10 (π‘ˆ ∈ 𝑉 β†’ (RingCatβ€˜π‘ˆ) ∈ Cat)
6463ad3antrrr 728 . . . . . . . . 9 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ (RingCatβ€˜π‘ˆ) ∈ Cat)
6514adantr 479 . . . . . . . . . 10 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ π‘₯ ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
6665adantr 479 . . . . . . . . 9 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ π‘₯ ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
6716ad2ant2r 745 . . . . . . . . . 10 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ 𝑦 ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
6867adantr 479 . . . . . . . . 9 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ 𝑦 ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
693, 1srhmsubclem2 20625 . . . . . . . . . . 11 ((π‘ˆ ∈ 𝑉 ∧ 𝑧 ∈ 𝐢) β†’ 𝑧 ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
7069ad2ant2rl 747 . . . . . . . . . 10 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ 𝑧 ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
7170adantr 479 . . . . . . . . 9 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ 𝑧 ∈ (Baseβ€˜(RingCatβ€˜π‘ˆ)))
7253adantr 479 . . . . . . . . . . . . . . 15 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ π‘ˆ ∈ 𝑉)
73 simpl 481 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢) β†’ 𝑦 ∈ 𝐢)
7458, 73anim12i 611 . . . . . . . . . . . . . . 15 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢))
7572, 74jca 510 . . . . . . . . . . . . . 14 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)))
763, 1, 20srhmsubclem3 20626 . . . . . . . . . . . . . 14 ((π‘ˆ ∈ 𝑉 ∧ (π‘₯ ∈ 𝐢 ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯𝐽𝑦) = (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑦))
7775, 76syl 17 . . . . . . . . . . . . 13 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (π‘₯𝐽𝑦) = (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑦))
7877eleq2d 2815 . . . . . . . . . . . 12 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (𝑓 ∈ (π‘₯𝐽𝑦) ↔ 𝑓 ∈ (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑦)))
7978biimpcd 248 . . . . . . . . . . 11 (𝑓 ∈ (π‘₯𝐽𝑦) β†’ (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ 𝑓 ∈ (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑦)))
8079adantr 479 . . . . . . . . . 10 ((𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)) β†’ (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ 𝑓 ∈ (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑦)))
8180impcom 406 . . . . . . . . 9 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ 𝑓 ∈ (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑦))
823, 1, 20srhmsubclem3 20626 . . . . . . . . . . . . . 14 ((π‘ˆ ∈ 𝑉 ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (𝑦𝐽𝑧) = (𝑦(Hom β€˜(RingCatβ€˜π‘ˆ))𝑧))
8382adantlr 713 . . . . . . . . . . . . 13 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (𝑦𝐽𝑧) = (𝑦(Hom β€˜(RingCatβ€˜π‘ˆ))𝑧))
8483eleq2d 2815 . . . . . . . . . . . 12 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (𝑔 ∈ (𝑦𝐽𝑧) ↔ 𝑔 ∈ (𝑦(Hom β€˜(RingCatβ€˜π‘ˆ))𝑧)))
8584biimpd 228 . . . . . . . . . . 11 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (𝑔 ∈ (𝑦𝐽𝑧) β†’ 𝑔 ∈ (𝑦(Hom β€˜(RingCatβ€˜π‘ˆ))𝑧)))
8685adantld 489 . . . . . . . . . 10 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ ((𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)) β†’ 𝑔 ∈ (𝑦(Hom β€˜(RingCatβ€˜π‘ˆ))𝑧)))
8786imp 405 . . . . . . . . 9 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ 𝑔 ∈ (𝑦(Hom β€˜(RingCatβ€˜π‘ˆ))𝑧))
8811, 13, 62, 64, 66, 68, 71, 81, 87catcocl 17674 . . . . . . . 8 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ (𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜(RingCatβ€˜π‘ˆ))𝑧)𝑓) ∈ (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑧))
8910, 11, 72, 13, 65, 70ringchom 20599 . . . . . . . . . 10 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑧) = (π‘₯ RingHom 𝑧))
9089eqcomd 2734 . . . . . . . . 9 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (π‘₯ RingHom 𝑧) = (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑧))
9190adantr 479 . . . . . . . 8 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ (π‘₯ RingHom 𝑧) = (π‘₯(Hom β€˜(RingCatβ€˜π‘ˆ))𝑧))
9288, 91eleqtrrd 2832 . . . . . . 7 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ (𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜(RingCatβ€˜π‘ˆ))𝑧)𝑓) ∈ (π‘₯ RingHom 𝑧))
9320a1i 11 . . . . . . . . 9 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ 𝐽 = (π‘Ÿ ∈ 𝐢, 𝑠 ∈ 𝐢 ↦ (π‘Ÿ RingHom 𝑠)))
94 oveq12 7435 . . . . . . . . . 10 ((π‘Ÿ = π‘₯ ∧ 𝑠 = 𝑧) β†’ (π‘Ÿ RingHom 𝑠) = (π‘₯ RingHom 𝑧))
9594adantl 480 . . . . . . . . 9 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (π‘Ÿ = π‘₯ ∧ 𝑠 = 𝑧)) β†’ (π‘Ÿ RingHom 𝑠) = (π‘₯ RingHom 𝑧))
9658adantr 479 . . . . . . . . 9 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ π‘₯ ∈ 𝐢)
97 simprr 771 . . . . . . . . 9 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ 𝑧 ∈ 𝐢)
98 ovexd 7461 . . . . . . . . 9 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (π‘₯ RingHom 𝑧) ∈ V)
9993, 95, 96, 97, 98ovmpod 7580 . . . . . . . 8 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ (π‘₯𝐽𝑧) = (π‘₯ RingHom 𝑧))
10099adantr 479 . . . . . . 7 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ (π‘₯𝐽𝑧) = (π‘₯ RingHom 𝑧))
10192, 100eleqtrrd 2832 . . . . . 6 ((((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) ∧ (𝑓 ∈ (π‘₯𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) β†’ (𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜(RingCatβ€˜π‘ˆ))𝑧)𝑓) ∈ (π‘₯𝐽𝑧))
102101ralrimivva 3198 . . . . 5 (((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) ∧ (𝑦 ∈ 𝐢 ∧ 𝑧 ∈ 𝐢)) β†’ βˆ€π‘“ ∈ (π‘₯𝐽𝑦)βˆ€π‘” ∈ (𝑦𝐽𝑧)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜(RingCatβ€˜π‘ˆ))𝑧)𝑓) ∈ (π‘₯𝐽𝑧))
103102ralrimivva 3198 . . . 4 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ βˆ€π‘¦ ∈ 𝐢 βˆ€π‘§ ∈ 𝐢 βˆ€π‘“ ∈ (π‘₯𝐽𝑦)βˆ€π‘” ∈ (𝑦𝐽𝑧)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜(RingCatβ€˜π‘ˆ))𝑧)𝑓) ∈ (π‘₯𝐽𝑧))
10461, 103jca 510 . . 3 ((π‘ˆ ∈ 𝑉 ∧ π‘₯ ∈ 𝐢) β†’ (((Idβ€˜(RingCatβ€˜π‘ˆ))β€˜π‘₯) ∈ (π‘₯𝐽π‘₯) ∧ βˆ€π‘¦ ∈ 𝐢 βˆ€π‘§ ∈ 𝐢 βˆ€π‘“ ∈ (π‘₯𝐽𝑦)βˆ€π‘” ∈ (𝑦𝐽𝑧)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜(RingCatβ€˜π‘ˆ))𝑧)𝑓) ∈ (π‘₯𝐽𝑧)))
105104ralrimiva 3143 . 2 (π‘ˆ ∈ 𝑉 β†’ βˆ€π‘₯ ∈ 𝐢 (((Idβ€˜(RingCatβ€˜π‘ˆ))β€˜π‘₯) ∈ (π‘₯𝐽π‘₯) ∧ βˆ€π‘¦ ∈ 𝐢 βˆ€π‘§ ∈ 𝐢 βˆ€π‘“ ∈ (π‘₯𝐽𝑦)βˆ€π‘” ∈ (𝑦𝐽𝑧)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜(RingCatβ€˜π‘ˆ))𝑧)𝑓) ∈ (π‘₯𝐽𝑧)))
10628, 52, 62, 63, 34issubc2 17831 . 2 (π‘ˆ ∈ 𝑉 β†’ (𝐽 ∈ (Subcatβ€˜(RingCatβ€˜π‘ˆ)) ↔ (𝐽 βŠ†cat (Homf β€˜(RingCatβ€˜π‘ˆ)) ∧ βˆ€π‘₯ ∈ 𝐢 (((Idβ€˜(RingCatβ€˜π‘ˆ))β€˜π‘₯) ∈ (π‘₯𝐽π‘₯) ∧ βˆ€π‘¦ ∈ 𝐢 βˆ€π‘§ ∈ 𝐢 βˆ€π‘“ ∈ (π‘₯𝐽𝑦)βˆ€π‘” ∈ (𝑦𝐽𝑧)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜(RingCatβ€˜π‘ˆ))𝑧)𝑓) ∈ (π‘₯𝐽𝑧)))))
10744, 105, 106mpbir2and 711 1 (π‘ˆ ∈ 𝑉 β†’ 𝐽 ∈ (Subcatβ€˜(RingCatβ€˜π‘ˆ)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  βˆ€wral 3058  Vcvv 3473   ∩ cin 3948   βŠ† wss 3949  βŸ¨cop 4638   class class class wbr 5152   I cid 5579   Γ— cxp 5680   β†Ύ cres 5684   Fn wfn 6548  β€˜cfv 6553  (class class class)co 7426   ∈ cmpo 7428  Basecbs 17189  Hom chom 17253  compcco 17254  Catccat 17653  Idccid 17654  Homf chomf 17655   βŠ†cat cssc 17799  Subcatcsubc 17801  Ringcrg 20187   RingHom crh 20422  RingCatcringc 20592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7879  df-1st 8001  df-2nd 8002  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-er 8733  df-map 8855  df-pm 8856  df-ixp 8925  df-en 8973  df-dom 8974  df-sdom 8975  df-fin 8976  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-nn 12253  df-2 12315  df-3 12316  df-4 12317  df-5 12318  df-6 12319  df-7 12320  df-8 12321  df-9 12322  df-n0 12513  df-z 12599  df-dec 12718  df-uz 12863  df-fz 13527  df-struct 17125  df-sets 17142  df-slot 17160  df-ndx 17172  df-base 17190  df-ress 17219  df-plusg 17255  df-hom 17266  df-cco 17267  df-0g 17432  df-cat 17657  df-cid 17658  df-homf 17659  df-ssc 17802  df-resc 17803  df-subc 17804  df-estrc 18122  df-mgm 18609  df-sgrp 18688  df-mnd 18704  df-mhm 18749  df-grp 18907  df-ghm 19182  df-mgp 20089  df-ur 20136  df-ring 20189  df-rhm 20425  df-ringc 20593
This theorem is referenced by:  sringcat  20628  crhmsubc  20629  drhmsubc  20683  fldhmsubc  20687
  Copyright terms: Public domain W3C validator