catcval

Description: Value of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	catcval.c	$⊢ C = CatCat (U)$
	catcval.u	$⊢ φ \to U \in V$
	catcval.b	$⊢ φ \to B = U \cap Cat$
	catcval.h	$⊢ φ \to H = (x \in B, y \in B ⟼ x Func y)$
	catcval.o	$⊢ φ \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))$
Assertion	catcval	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Proof

Step	Hyp	Ref	Expression
1		catcval.c	$⊢ C = CatCat (U)$
2		catcval.u	$⊢ φ \to U \in V$
3		catcval.b	$⊢ φ \to B = U \cap Cat$
4		catcval.h	$⊢ φ \to H = (x \in B, y \in B ⟼ x Func y)$
5		catcval.o	$⊢ φ \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))$
6		df-catc	$⊢ CatCat = (u \in V ⟼ ⦋ (u \cap Cat) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x Func y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\})$
7		vex	$⊢ u \in V$
8	7	inex1	$⊢ u \cap Cat \in V$
9	8	a1i	$⊢ (φ \land u = U) \to u \cap Cat \in V$
10		simpr	$⊢ (φ \land u = U) \to u = U$
11	10	ineq1d	$⊢ (φ \land u = U) \to u \cap Cat = U \cap Cat$
12	3	adantr	$⊢ (φ \land u = U) \to B = U \cap Cat$
13	11 12	eqtr4d	$⊢ (φ \land u = U) \to u \cap Cat = B$
14		simpr	$⊢ ((φ \land u = U) \land b = B) \to b = B$
15	14	opeq2d	$⊢ ((φ \land u = U) \land b = B) \to ⟨{Base}_{ndx}, b⟩ = ⟨{Base}_{ndx}, B⟩$
16		eqidd	$⊢ ((φ \land u = U) \land b = B) \to x Func y = x Func y$
17	14 14 16	mpoeq123dv	$⊢ ((φ \land u = U) \land b = B) \to (x \in b, y \in b ⟼ x Func y) = (x \in B, y \in B ⟼ x Func y)$
18	4	ad2antrr	$⊢ ((φ \land u = U) \land b = B) \to H = (x \in B, y \in B ⟼ x Func y)$
19	17 18	eqtr4d	$⊢ ((φ \land u = U) \land b = B) \to (x \in b, y \in b ⟼ x Func y) = H$
20	19	opeq2d	$⊢ ((φ \land u = U) \land b = B) \to ⟨Hom (ndx), (x \in b, y \in b ⟼ x Func y)⟩ = ⟨Hom (ndx), H⟩$
21	14	sqxpeqd	$⊢ ((φ \land u = U) \land b = B) \to b \times b = B \times B$
22		eqidd	$⊢ ((φ \land u = U) \land b = B) \to (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f) = (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f)$
23	21 14 22	mpoeq123dv	$⊢ ((φ \land u = U) \land b = B) \to (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f)) = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))$
24	5	ad2antrr	$⊢ ((φ \land u = U) \land b = B) \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))$
25	23 24	eqtr4d	$⊢ ((φ \land u = U) \land b = B) \to (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f)) = \underset{˙}{\cdot}$
26	25	opeq2d	$⊢ ((φ \land u = U) \land b = B) \to ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩ = ⟨comp (ndx), \underset{˙}{\cdot}⟩$
27	15 20 26	tpeq123d	$⊢ ((φ \land u = U) \land b = B) \to \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x Func y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
28	9 13 27	csbied2	$⊢ (φ \land u = U) \to ⦋ (u \cap Cat) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x Func y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
29	2	elexd	$⊢ φ \to U \in V$
30		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
31	30	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
32	6 28 29 31	fvmptd2	$⊢ φ \to CatCat (U) = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
33	1 32	syl5eq	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Metamath Proof Explorer

Theorem catcval

Proof