Metamath Proof Explorer

Theorem rngcbasALTV

Description: Set of objects of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 rngcbasALTV.c ⊢ C = RngCatALTV ⁡ U
2 rngcbasALTV.b ⊢ B = Base C
3 rngcbasALTV.u ⊢ φ → U ∈ V
4 eqidd ⊢ φ → U ∩ Rng = U ∩ Rng
5 eqidd ⊢ φ → x ∈ U ∩ Rng , y ∈ U ∩ Rng ⟼ x RngHom y = x ∈ U ∩ Rng , y ∈ U ∩ Rng ⟼ x RngHom y
6 eqidd ⊢ φ → v ∈ U ∩ Rng × U ∩ Rng , z ∈ U ∩ Rng ⟼ f ∈ 2 nd ⁡ v RngHom z , g ∈ 1 st ⁡ v RngHom 2 nd ⁡ v ⟼ f ∘ g = v ∈ U ∩ Rng × U ∩ Rng , z ∈ U ∩ Rng ⟼ f ∈ 2 nd ⁡ v RngHom z , g ∈ 1 st ⁡ v RngHom 2 nd ⁡ v ⟼ f ∘ g
7 1 3 4 5 6 rngcvalALTV ⊢ φ → C = Base ndx U ∩ Rng Hom ⁡ ndx x ∈ U ∩ Rng , y ∈ U ∩ Rng ⟼ x RngHom y comp ⁡ ndx v ∈ U ∩ Rng × U ∩ Rng , z ∈ U ∩ Rng ⟼ f ∈ 2 nd ⁡ v RngHom z , g ∈ 1 st ⁡ v RngHom 2 nd ⁡ v ⟼ f ∘ g
8 catstr ⊢ Base ndx U ∩ Rng Hom ⁡ ndx x ∈ U ∩ Rng , y ∈ U ∩ Rng ⟼ x RngHom y comp ⁡ ndx v ∈ U ∩ Rng × U ∩ Rng , z ∈ U ∩ Rng ⟼ f ∈ 2 nd ⁡ v RngHom z , g ∈ 1 st ⁡ v RngHom 2 nd ⁡ v ⟼ f ∘ g Struct 1 15
9 baseid ⊢ Base = Slot Base ndx
10 snsstp1 ⊢ Base ndx U ∩ Rng ⊆ Base ndx U ∩ Rng Hom ⁡ ndx x ∈ U ∩ Rng , y ∈ U ∩ Rng ⟼ x RngHom y comp ⁡ ndx v ∈ U ∩ Rng × U ∩ Rng , z ∈ U ∩ Rng ⟼ f ∈ 2 nd ⁡ v RngHom z , g ∈ 1 st ⁡ v RngHom 2 nd ⁡ v ⟼ f ∘ g
11 inex1g ⊢ U ∈ V → U ∩ Rng ∈ V
12 3 11 syl ⊢ φ → U ∩ Rng ∈ V
13 7 8 9 10 12 2 strfv3 ⊢ φ → B = U ∩ Rng