Metamath Proof Explorer

Theorem ringcbasALTV

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

Ref Expression
Hypotheses ringcbasALTV.c ⊢ C = RingCatALTV ⁡ U
ringcbasALTV.b ⊢ B = Base C
ringcbasALTV.u ⊢ φ → U ∈ V
Assertion ringcbasALTV ⊢ φ → B = U ∩ Ring

Proof

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