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	$⊢ φ \to U \in V$
	Assertion	rngcbasALTV	$⊢ φ \to B = U \cap Rng$

Proof

Step	Hyp	Ref	Expression
1		rngcbasALTV.c	$⊢ C = RngCatALTV (U)$
2		rngcbasALTV.b	$⊢ B = {Base}_{C}$
3		rngcbasALTV.u	$⊢ φ \to U \in V$
4		eqidd	$⊢ φ \to U \cap Rng = U \cap Rng$
5		eqidd	$⊢ φ \to (x \in (U \cap Rng), y \in (U \cap Rng) ⟼ x RngHom y) = (x \in (U \cap Rng), y \in (U \cap Rng) ⟼ x RngHom y)$
6		eqidd	$⊢ φ \to (v \in ((U \cap Rng) \times (U \cap Rng)), z \in (U \cap Rng) ⟼ (f \in (2^{nd} (v) RngHom z), g \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ f \circ g)) = (v \in ((U \cap Rng) \times (U \cap Rng)), z \in (U \cap Rng) ⟼ (f \in (2^{nd} (v) RngHom z), g \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ f \circ g))$
7	1 3 4 5 6	rngcvalALTV	$⊢ φ \to C = \{⟨{Base}_{ndx}, U \cap Rng⟩, ⟨Hom (ndx), (x \in (U \cap Rng), y \in (U \cap Rng) ⟼ x RngHom y)⟩, ⟨comp (ndx), (v \in ((U \cap Rng) \times (U \cap Rng)), z \in (U \cap Rng) ⟼ (f \in (2^{nd} (v) RngHom z), g \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ f \circ g))⟩\}$
8		catstr	$⊢ \{⟨{Base}_{ndx}, U \cap Rng⟩, ⟨Hom (ndx), (x \in (U \cap Rng), y \in (U \cap Rng) ⟼ x RngHom y)⟩, ⟨comp (ndx), (v \in ((U \cap Rng) \times (U \cap Rng)), z \in (U \cap Rng) ⟼ (f \in (2^{nd} (v) RngHom z), g \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ f \circ g))⟩\} Struct ⟨1, 15⟩$
9		baseid	$⊢ Base = Slot {Base}_{ndx}$
10		snsstp1	$⊢ \{⟨{Base}_{ndx}, U \cap Rng⟩\} \subseteq \{⟨{Base}_{ndx}, U \cap Rng⟩, ⟨Hom (ndx), (x \in (U \cap Rng), y \in (U \cap Rng) ⟼ x RngHom y)⟩, ⟨comp (ndx), (v \in ((U \cap Rng) \times (U \cap Rng)), z \in (U \cap Rng) ⟼ (f \in (2^{nd} (v) RngHom z), g \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ f \circ g))⟩\}$
11		inex1g	$⊢ U \in V \to U \cap Rng \in V$
12	3 11	syl	$⊢ φ \to U \cap Rng \in V$
13	7 8 9 10 12 2	strfv3	$⊢ φ \to B = U \cap Rng$