| Step | Hyp | Ref
| Expression |
| 1 | | srhmsubc.c |
. . . 4
⊢ 𝐶 = (𝑈 ∩ 𝑆) |
| 2 | | eleq1w 2824 |
. . . . . . 7
⊢ (𝑟 = 𝑥 → (𝑟 ∈ Ring ↔ 𝑥 ∈ Ring)) |
| 3 | | srhmsubc.s |
. . . . . . 7
⊢
∀𝑟 ∈
𝑆 𝑟 ∈ Ring |
| 4 | 2, 3 | vtoclri 3590 |
. . . . . 6
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ Ring) |
| 5 | 4 | ssriv 3987 |
. . . . 5
⊢ 𝑆 ⊆ Ring |
| 6 | | sslin 4243 |
. . . . 5
⊢ (𝑆 ⊆ Ring → (𝑈 ∩ 𝑆) ⊆ (𝑈 ∩ Ring)) |
| 7 | 5, 6 | mp1i 13 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ 𝑆) ⊆ (𝑈 ∩ Ring)) |
| 8 | 1, 7 | eqsstrid 4022 |
. . 3
⊢ (𝑈 ∈ 𝑉 → 𝐶 ⊆ (𝑈 ∩ Ring)) |
| 9 | | ssid 4006 |
. . . . . 6
⊢ (𝑥 RingHom 𝑦) ⊆ (𝑥 RingHom 𝑦) |
| 10 | | eqid 2737 |
. . . . . . 7
⊢
(RingCat‘𝑈) =
(RingCat‘𝑈) |
| 11 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(RingCat‘𝑈)) = (Base‘(RingCat‘𝑈)) |
| 12 | | simpl 482 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑈 ∈ 𝑉) |
| 13 | | eqid 2737 |
. . . . . . 7
⊢ (Hom
‘(RingCat‘𝑈)) =
(Hom ‘(RingCat‘𝑈)) |
| 14 | 3, 1 | srhmsubclem2 20678 |
. . . . . . . 8
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ (Base‘(RingCat‘𝑈))) |
| 15 | 14 | adantrr 717 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (Base‘(RingCat‘𝑈))) |
| 16 | 3, 1 | srhmsubclem2 20678 |
. . . . . . . 8
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ (Base‘(RingCat‘𝑈))) |
| 17 | 16 | adantrl 716 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ (Base‘(RingCat‘𝑈))) |
| 18 | 10, 11, 12, 13, 15, 17 | ringchom 20652 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(Hom ‘(RingCat‘𝑈))𝑦) = (𝑥 RingHom 𝑦)) |
| 19 | 9, 18 | sseqtrrid 4027 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 RingHom 𝑦) ⊆ (𝑥(Hom ‘(RingCat‘𝑈))𝑦)) |
| 20 | | srhmsubc.j |
. . . . . . 7
⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠)) |
| 21 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))) |
| 22 | | oveq12 7440 |
. . . . . . 7
⊢ ((𝑟 = 𝑥 ∧ 𝑠 = 𝑦) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑦)) |
| 23 | 22 | adantl 481 |
. . . . . 6
⊢ (((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) ∧ (𝑟 = 𝑥 ∧ 𝑠 = 𝑦)) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑦)) |
| 24 | | simprl 771 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ 𝐶) |
| 25 | | simprr 773 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶) |
| 26 | | ovexd 7466 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 RingHom 𝑦) ∈ V) |
| 27 | 21, 23, 24, 25, 26 | ovmpod 7585 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥𝐽𝑦) = (𝑥 RingHom 𝑦)) |
| 28 | | eqid 2737 |
. . . . . 6
⊢
(Homf ‘(RingCat‘𝑈)) = (Homf
‘(RingCat‘𝑈)) |
| 29 | 28, 11, 13, 15, 17 | homfval 17735 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(Homf
‘(RingCat‘𝑈))𝑦) = (𝑥(Hom ‘(RingCat‘𝑈))𝑦)) |
| 30 | 19, 27, 29 | 3sstr4d 4039 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥𝐽𝑦) ⊆ (𝑥(Homf
‘(RingCat‘𝑈))𝑦)) |
| 31 | 30 | ralrimivva 3202 |
. . 3
⊢ (𝑈 ∈ 𝑉 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝐽𝑦) ⊆ (𝑥(Homf
‘(RingCat‘𝑈))𝑦)) |
| 32 | | ovex 7464 |
. . . . . 6
⊢ (𝑟 RingHom 𝑠) ∈ V |
| 33 | 20, 32 | fnmpoi 8095 |
. . . . 5
⊢ 𝐽 Fn (𝐶 × 𝐶) |
| 34 | 33 | a1i 11 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝐽 Fn (𝐶 × 𝐶)) |
| 35 | 28, 11 | homffn 17736 |
. . . . 5
⊢
(Homf ‘(RingCat‘𝑈)) Fn ((Base‘(RingCat‘𝑈)) ×
(Base‘(RingCat‘𝑈))) |
| 36 | | id 22 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ 𝑉) |
| 37 | 10, 11, 36 | ringcbas 20650 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑉 → (Base‘(RingCat‘𝑈)) = (𝑈 ∩ Ring)) |
| 38 | 37 | eqcomd 2743 |
. . . . . . 7
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ Ring) =
(Base‘(RingCat‘𝑈))) |
| 39 | 38 | sqxpeqd 5717 |
. . . . . 6
⊢ (𝑈 ∈ 𝑉 → ((𝑈 ∩ Ring) × (𝑈 ∩ Ring)) =
((Base‘(RingCat‘𝑈)) × (Base‘(RingCat‘𝑈)))) |
| 40 | 39 | fneq2d 6662 |
. . . . 5
⊢ (𝑈 ∈ 𝑉 → ((Homf
‘(RingCat‘𝑈))
Fn ((𝑈 ∩ Ring) ×
(𝑈 ∩ Ring)) ↔
(Homf ‘(RingCat‘𝑈)) Fn ((Base‘(RingCat‘𝑈)) ×
(Base‘(RingCat‘𝑈))))) |
| 41 | 35, 40 | mpbiri 258 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (Homf
‘(RingCat‘𝑈))
Fn ((𝑈 ∩ Ring) ×
(𝑈 ∩
Ring))) |
| 42 | | inex1g 5319 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ Ring) ∈ V) |
| 43 | 34, 41, 42 | isssc 17864 |
. . 3
⊢ (𝑈 ∈ 𝑉 → (𝐽 ⊆cat
(Homf ‘(RingCat‘𝑈)) ↔ (𝐶 ⊆ (𝑈 ∩ Ring) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝐽𝑦) ⊆ (𝑥(Homf
‘(RingCat‘𝑈))𝑦)))) |
| 44 | 8, 31, 43 | mpbir2and 713 |
. 2
⊢ (𝑈 ∈ 𝑉 → 𝐽 ⊆cat
(Homf ‘(RingCat‘𝑈))) |
| 45 | 1 | elin2 4203 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐶 ↔ (𝑥 ∈ 𝑈 ∧ 𝑥 ∈ 𝑆)) |
| 46 | 4 | adantl 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑈 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ Ring) |
| 47 | 45, 46 | sylbi 217 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ Ring) |
| 48 | 47 | adantl 481 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ Ring) |
| 49 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑥) =
(Base‘𝑥) |
| 50 | 49 | idrhm 20490 |
. . . . . 6
⊢ (𝑥 ∈ Ring → ( I ↾
(Base‘𝑥)) ∈
(𝑥 RingHom 𝑥)) |
| 51 | 48, 50 | syl 17 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ( I ↾ (Base‘𝑥)) ∈ (𝑥 RingHom 𝑥)) |
| 52 | | eqid 2737 |
. . . . . 6
⊢
(Id‘(RingCat‘𝑈)) = (Id‘(RingCat‘𝑈)) |
| 53 | | simpl 482 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑈 ∈ 𝑉) |
| 54 | 10, 11, 52, 53, 14, 49 | ringcid 20664 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ((Id‘(RingCat‘𝑈))‘𝑥) = ( I ↾ (Base‘𝑥))) |
| 55 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))) |
| 56 | | oveq12 7440 |
. . . . . . 7
⊢ ((𝑟 = 𝑥 ∧ 𝑠 = 𝑥) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑥)) |
| 57 | 56 | adantl 481 |
. . . . . 6
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑟 = 𝑥 ∧ 𝑠 = 𝑥)) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑥)) |
| 58 | | simpr 484 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) |
| 59 | | ovexd 7466 |
. . . . . 6
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → (𝑥 RingHom 𝑥) ∈ V) |
| 60 | 55, 57, 58, 58, 59 | ovmpod 7585 |
. . . . 5
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → (𝑥𝐽𝑥) = (𝑥 RingHom 𝑥)) |
| 61 | 51, 54, 60 | 3eltr4d 2856 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ((Id‘(RingCat‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥)) |
| 62 | | eqid 2737 |
. . . . . . . . 9
⊢
(comp‘(RingCat‘𝑈)) = (comp‘(RingCat‘𝑈)) |
| 63 | 10 | ringccat 20663 |
. . . . . . . . . 10
⊢ (𝑈 ∈ 𝑉 → (RingCat‘𝑈) ∈ Cat) |
| 64 | 63 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (RingCat‘𝑈) ∈ Cat) |
| 65 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑥 ∈ (Base‘(RingCat‘𝑈))) |
| 66 | 65 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑥 ∈ (Base‘(RingCat‘𝑈))) |
| 67 | 16 | ad2ant2r 747 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ (Base‘(RingCat‘𝑈))) |
| 68 | 67 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑦 ∈ (Base‘(RingCat‘𝑈))) |
| 69 | 3, 1 | srhmsubclem2 20678 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ (Base‘(RingCat‘𝑈))) |
| 70 | 69 | ad2ant2rl 749 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ (Base‘(RingCat‘𝑈))) |
| 71 | 70 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑧 ∈ (Base‘(RingCat‘𝑈))) |
| 72 | 53 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑈 ∈ 𝑉) |
| 73 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶) → 𝑦 ∈ 𝐶) |
| 74 | 58, 73 | anim12i 613 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) |
| 75 | 72, 74 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶))) |
| 76 | 3, 1, 20 | srhmsubclem3 20679 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥𝐽𝑦) = (𝑥(Hom ‘(RingCat‘𝑈))𝑦)) |
| 77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥𝐽𝑦) = (𝑥(Hom ‘(RingCat‘𝑈))𝑦)) |
| 78 | 77 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑓 ∈ (𝑥𝐽𝑦) ↔ 𝑓 ∈ (𝑥(Hom ‘(RingCat‘𝑈))𝑦))) |
| 79 | 78 | biimpcd 249 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝑥𝐽𝑦) → (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑓 ∈ (𝑥(Hom ‘(RingCat‘𝑈))𝑦))) |
| 80 | 79 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)) → (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑓 ∈ (𝑥(Hom ‘(RingCat‘𝑈))𝑦))) |
| 81 | 80 | impcom 407 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(RingCat‘𝑈))𝑦)) |
| 82 | 3, 1, 20 | srhmsubclem3 20679 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ 𝑉 ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑦𝐽𝑧) = (𝑦(Hom ‘(RingCat‘𝑈))𝑧)) |
| 83 | 82 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑦𝐽𝑧) = (𝑦(Hom ‘(RingCat‘𝑈))𝑧)) |
| 84 | 83 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑔 ∈ (𝑦𝐽𝑧) ↔ 𝑔 ∈ (𝑦(Hom ‘(RingCat‘𝑈))𝑧))) |
| 85 | 84 | biimpd 229 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑔 ∈ (𝑦𝐽𝑧) → 𝑔 ∈ (𝑦(Hom ‘(RingCat‘𝑈))𝑧))) |
| 86 | 85 | adantld 490 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → ((𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)) → 𝑔 ∈ (𝑦(Hom ‘(RingCat‘𝑈))𝑧))) |
| 87 | 86 | imp 406 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(RingCat‘𝑈))𝑧)) |
| 88 | 11, 13, 62, 64, 66, 68, 71, 81, 87 | catcocl 17728 |
. . . . . . . 8
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RingCat‘𝑈))𝑧)𝑓) ∈ (𝑥(Hom ‘(RingCat‘𝑈))𝑧)) |
| 89 | 10, 11, 72, 13, 65, 70 | ringchom 20652 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥(Hom ‘(RingCat‘𝑈))𝑧) = (𝑥 RingHom 𝑧)) |
| 90 | 89 | eqcomd 2743 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥 RingHom 𝑧) = (𝑥(Hom ‘(RingCat‘𝑈))𝑧)) |
| 91 | 90 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑥 RingHom 𝑧) = (𝑥(Hom ‘(RingCat‘𝑈))𝑧)) |
| 92 | 88, 91 | eleqtrrd 2844 |
. . . . . . 7
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RingCat‘𝑈))𝑧)𝑓) ∈ (𝑥 RingHom 𝑧)) |
| 93 | 20 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))) |
| 94 | | oveq12 7440 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑥 ∧ 𝑠 = 𝑧) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑧)) |
| 95 | 94 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑟 = 𝑥 ∧ 𝑠 = 𝑧)) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑧)) |
| 96 | 58 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑥 ∈ 𝐶) |
| 97 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐶) |
| 98 | | ovexd 7466 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥 RingHom 𝑧) ∈ V) |
| 99 | 93, 95, 96, 97, 98 | ovmpod 7585 |
. . . . . . . 8
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑥𝐽𝑧) = (𝑥 RingHom 𝑧)) |
| 100 | 99 | adantr 480 |
. . . . . . 7
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑥𝐽𝑧) = (𝑥 RingHom 𝑧)) |
| 101 | 92, 100 | eleqtrrd 2844 |
. . . . . 6
⊢ ((((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RingCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
| 102 | 101 | ralrimivva 3202 |
. . . . 5
⊢ (((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
| 103 | 102 | ralrimivva 3202 |
. . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
| 104 | 61, 103 | jca 511 |
. . 3
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝐶) → (((Id‘(RingCat‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧))) |
| 105 | 104 | ralrimiva 3146 |
. 2
⊢ (𝑈 ∈ 𝑉 → ∀𝑥 ∈ 𝐶 (((Id‘(RingCat‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧))) |
| 106 | 28, 52, 62, 63, 34 | issubc2 17881 |
. 2
⊢ (𝑈 ∈ 𝑉 → (𝐽 ∈ (Subcat‘(RingCat‘𝑈)) ↔ (𝐽 ⊆cat
(Homf ‘(RingCat‘𝑈)) ∧ ∀𝑥 ∈ 𝐶 (((Id‘(RingCat‘𝑈))‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘(RingCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) |
| 107 | 44, 105, 106 | mpbir2and 713 |
1
⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCat‘𝑈))) |