setcval

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

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

Proof

Step	Hyp	Ref	Expression
1		setcval.c	$⊢ C = SetCat (U)$
2		setcval.u	$⊢ φ \to U \in V$
3		setcval.h	$⊢ φ \to H = (x \in U, y \in U ⟼ y^{x})$
4		setcval.o	$⊢ φ \to \underset{˙}{\cdot} = (v \in (U \times U), z \in U ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))$
5		df-setc	$⊢ SetCat = (u \in V ⟼ \{⟨{Base}_{ndx}, u⟩, ⟨Hom (ndx), (x \in u, y \in u ⟼ y^{x})⟩, ⟨comp (ndx), (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))⟩\})$
6		simpr	$⊢ (φ \land u = U) \to u = U$
7	6	opeq2d	$⊢ (φ \land u = U) \to ⟨{Base}_{ndx}, u⟩ = ⟨{Base}_{ndx}, U⟩$
8		eqidd	$⊢ (φ \land u = U) \to y^{x} = y^{x}$
9	6 6 8	mpoeq123dv	$⊢ (φ \land u = U) \to (x \in u, y \in u ⟼ y^{x}) = (x \in U, y \in U ⟼ y^{x})$
10	3	adantr	$⊢ (φ \land u = U) \to H = (x \in U, y \in U ⟼ y^{x})$
11	9 10	eqtr4d	$⊢ (φ \land u = U) \to (x \in u, y \in u ⟼ y^{x}) = H$
12	11	opeq2d	$⊢ (φ \land u = U) \to ⟨Hom (ndx), (x \in u, y \in u ⟼ y^{x})⟩ = ⟨Hom (ndx), H⟩$
13	6	sqxpeqd	$⊢ (φ \land u = U) \to u \times u = U \times U$
14		eqidd	$⊢ (φ \land u = U) \to (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f) = (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f)$
15	13 6 14	mpoeq123dv	$⊢ (φ \land u = U) \to (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f)) = (v \in (U \times U), z \in U ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))$
16	4	adantr	$⊢ (φ \land u = U) \to \underset{˙}{\cdot} = (v \in (U \times U), z \in U ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))$
17	15 16	eqtr4d	$⊢ (φ \land u = U) \to (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f)) = \underset{˙}{\cdot}$
18	17	opeq2d	$⊢ (φ \land u = U) \to ⟨comp (ndx), (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))⟩ = ⟨comp (ndx), \underset{˙}{\cdot}⟩$
19	7 12 18	tpeq123d	$⊢ (φ \land u = U) \to \{⟨{Base}_{ndx}, u⟩, ⟨Hom (ndx), (x \in u, y \in u ⟼ y^{x})⟩, ⟨comp (ndx), (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))⟩\} = \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
20	2	elexd	$⊢ φ \to U \in V$
21		tpex	$⊢ \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
22	21	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
23	5 19 20 22	fvmptd2	$⊢ φ \to SetCat (U) = \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
24	1 23	syl5eq	$⊢ φ \to C = \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Metamath Proof Explorer

Theorem setcval

Proof