Metamath Proof Explorer

Theorem rnghmsubcsetc

Description: The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020)

Ref Expression
Hypotheses rnghmsubcsetc.c ⊢ C = ExtStrCat ⁡ U
rnghmsubcsetc.u ⊢ φ → U ∈ V
rnghmsubcsetc.b ⊢ φ → B = Rng ∩ U
rnghmsubcsetc.h ⊢ φ → H = RngHomo ↾ B × B
Assertion rnghmsubcsetc ⊢ φ → H ∈ Subcat ⁡ C

Proof

Step Hyp Ref Expression
1 rnghmsubcsetc.c ⊢ C = ExtStrCat ⁡ U
2 rnghmsubcsetc.u ⊢ φ → U ∈ V
3 rnghmsubcsetc.b ⊢ φ → B = Rng ∩ U
4 rnghmsubcsetc.h ⊢ φ → H = RngHomo ↾ B × B
5 2 3 rnghmsscmap ⊢ φ → RngHomo ↾ B × B ⊆ cat x ∈ U , y ∈ U ⟼ Base y Base x
6 eqid ⊢ Hom ⁡ C = Hom ⁡ C
7 1 2 6 estrchomfeqhom ⊢ φ → Hom 𝑓 ⁡ C = Hom ⁡ C
8 1 2 6 estrchomfval ⊢ φ → Hom ⁡ C = x ∈ U , y ∈ U ⟼ Base y Base x
9 7 8 eqtrd ⊢ φ → Hom 𝑓 ⁡ C = x ∈ U , y ∈ U ⟼ Base y Base x
10 5 4 9 3brtr4d ⊢ φ → H ⊆ cat Hom 𝑓 ⁡ C
11 1 2 3 4 rnghmsubcsetclem1 ⊢ φ ∧ x ∈ B → Id ⁡ C ⁡ x ∈ x H x
12 1 2 3 4 rnghmsubcsetclem2 ⊢ φ ∧ x ∈ B → ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ C z f ∈ x H z
13 11 12 jca ⊢ φ ∧ x ∈ B → Id ⁡ C ⁡ x ∈ x H x ∧ ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ C z f ∈ x H z
14 13 ralrimiva ⊢ φ → ∀ x ∈ B Id ⁡ C ⁡ x ∈ x H x ∧ ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ C z f ∈ x H z
15 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
16 eqid ⊢ Id ⁡ C = Id ⁡ C
17 eqid ⊢ comp ⁡ C = comp ⁡ C
18 1 estrccat ⊢ U ∈ V → C ∈ Cat
19 2 18 syl ⊢ φ → C ∈ Cat
20 incom ⊢ Rng ∩ U = U ∩ Rng
21 3 20 eqtrdi ⊢ φ → B = U ∩ Rng
22 21 4 rnghmresfn ⊢ φ → H Fn B × B
23 15 16 17 19 22 issubc2 ⊢ φ → H ∈ Subcat ⁡ C ↔ H ⊆ cat Hom 𝑓 ⁡ C ∧ ∀ x ∈ B Id ⁡ C ⁡ x ∈ x H x ∧ ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y comp ⁡ C z f ∈ x H z
24 10 14 23 mpbir2and ⊢ φ → H ∈ Subcat ⁡ C