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

Metamath Proof Explorer

Theorem rngcbas

Description: Set of objects of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020) (Revised by AV, 8-Mar-2020)

Ref Expression
Hypotheses rngcbas.c ⊢ C = RngCat ⁡ U
rngcbas.b ⊢ B = Base C
rngcbas.u ⊢ φ → U ∈ V
Assertion rngcbas ⊢ φ → B = U ∩ Rng

Proof

Step Hyp Ref Expression
1 rngcbas.c ⊢ C = RngCat ⁡ U
2 rngcbas.b ⊢ B = Base C
3 rngcbas.u ⊢ φ → U ∈ V
4 eqidd ⊢ φ → U ∩ Rng = U ∩ Rng
5 eqidd ⊢ φ → RngHom ↾ U ∩ Rng × U ∩ Rng = RngHom ↾ U ∩ Rng × U ∩ Rng
6 1 3 4 5 rngcval ⊢ φ → C = ExtStrCat ⁡ U ↾ cat RngHom ↾ U ∩ Rng × U ∩ Rng
7 6 fveq2d ⊢ φ → Base C = Base ExtStrCat ⁡ U ↾ cat RngHom ↾ U ∩ Rng × U ∩ Rng
8 2 a1i ⊢ φ → B = Base C
9 eqid ⊢ ExtStrCat ⁡ U ↾ cat RngHom ↾ U ∩ Rng × U ∩ Rng = ExtStrCat ⁡ U ↾ cat RngHom ↾ U ∩ Rng × U ∩ Rng
10 eqid ⊢ Base ExtStrCat ⁡ U = Base ExtStrCat ⁡ U
11 fvexd ⊢ φ → ExtStrCat ⁡ U ∈ V
12 4 5 rnghmresfn ⊢ φ → RngHom ↾ U ∩ Rng × U ∩ Rng Fn U ∩ Rng × U ∩ Rng
13 inss1 ⊢ U ∩ Rng ⊆ U
14 eqid ⊢ ExtStrCat ⁡ U = ExtStrCat ⁡ U
15 14 3 estrcbas ⊢ φ → U = Base ExtStrCat ⁡ U
16 13 15 sseqtrid ⊢ φ → U ∩ Rng ⊆ Base ExtStrCat ⁡ U
17 9 10 11 12 16 rescbas ⊢ φ → U ∩ Rng = Base ExtStrCat ⁡ U ↾ cat RngHom ↾ U ∩ Rng × U ∩ Rng
18 7 8 17 3eqtr4d ⊢ φ → B = U ∩ Rng