ringcvalALTV

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

	Ref	Expression
Hypotheses	ringcvalALTV.c	$⊢ C = RingCatALTV (U)$
	ringcvalALTV.u	$⊢ φ \to U \in V$
	ringcvalALTV.b	$⊢ φ \to B = U \cap Ring$
	ringcvalALTV.h	$⊢ φ \to H = (x \in B, y \in B ⟼ x RingHom y)$
	ringcvalALTV.o	$⊢ φ \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))$
Assertion	ringcvalALTV	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Proof

Step	Hyp	Ref	Expression
1		ringcvalALTV.c	$⊢ C = RingCatALTV (U)$
2		ringcvalALTV.u	$⊢ φ \to U \in V$
3		ringcvalALTV.b	$⊢ φ \to B = U \cap Ring$
4		ringcvalALTV.h	$⊢ φ \to H = (x \in B, y \in B ⟼ x RingHom y)$
5		ringcvalALTV.o	$⊢ φ \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))$
6		df-ringcALTV	$⊢ RingCatALTV = (u \in V ⟼ ⦋ (u \cap Ring) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩\})$
7	6	a1i	$⊢ φ \to RingCatALTV = (u \in V ⟼ ⦋ (u \cap Ring) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩\})$
8		vex	$⊢ u \in V$
9	8	inex1	$⊢ u \cap Ring \in V$
10	9	a1i	$⊢ (φ \land u = U) \to u \cap Ring \in V$
11		ineq1	$⊢ u = U \to u \cap Ring = U \cap Ring$
12	11	adantl	$⊢ (φ \land u = U) \to u \cap Ring = U \cap Ring$
13	3	adantr	$⊢ (φ \land u = U) \to B = U \cap Ring$
14	12 13	eqtr4d	$⊢ (φ \land u = U) \to u \cap Ring = B$
15		simpr	$⊢ ((φ \land u = U) \land b = B) \to b = B$
16	15	opeq2d	$⊢ ((φ \land u = U) \land b = B) \to ⟨{Base}_{ndx}, b⟩ = ⟨{Base}_{ndx}, B⟩$
17		eqidd	$⊢ ((φ \land u = U) \land b = B) \to x RingHom y = x RingHom y$
18	15 15 17	mpoeq123dv	$⊢ ((φ \land u = U) \land b = B) \to (x \in b, y \in b ⟼ x RingHom y) = (x \in B, y \in B ⟼ x RingHom y)$
19	4	ad2antrr	$⊢ ((φ \land u = U) \land b = B) \to H = (x \in B, y \in B ⟼ x RingHom y)$
20	18 19	eqtr4d	$⊢ ((φ \land u = U) \land b = B) \to (x \in b, y \in b ⟼ x RingHom y) = H$
21	20	opeq2d	$⊢ ((φ \land u = U) \land b = B) \to ⟨Hom (ndx), (x \in b, y \in b ⟼ x RingHom y)⟩ = ⟨Hom (ndx), H⟩$
22	15	sqxpeqd	$⊢ ((φ \land u = U) \land b = B) \to b \times b = B \times B$
23		eqidd	$⊢ ((φ \land u = U) \land b = B) \to (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f) = (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f)$
24	22 15 23	mpoeq123dv	$⊢ ((φ \land u = U) \land b = B) \to (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f)) = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))$
25	5	ad2antrr	$⊢ ((φ \land u = U) \land b = B) \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))$
26	24 25	eqtr4d	$⊢ ((φ \land u = U) \land b = B) \to (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f)) = \underset{˙}{\cdot}$
27	26	opeq2d	$⊢ ((φ \land u = U) \land b = B) \to ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩ = ⟨comp (ndx), \underset{˙}{\cdot}⟩$
28	16 21 27	tpeq123d	$⊢ ((φ \land u = U) \land b = B) \to \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
29	10 14 28	csbied2	$⊢ (φ \land u = U) \to ⦋ (u \cap Ring) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
30		elex	$⊢ U \in V \to U \in V$
31	2 30	syl	$⊢ φ \to U \in V$
32		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
33	32	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
34	7 29 31 33	fvmptd	$⊢ φ \to RingCatALTV (U) = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
35	1 34	eqtrid	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Metamath Proof Explorer

Theorem ringcvalALTV

Proof