Metamath Proof Explorer

Theorem setcbas

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

		Ref	Expression
	Hypotheses	setcbas.c	$⊢ C = SetCat (U)$
		setcbas.u	$⊢ φ \to U \in V$
	Assertion	setcbas	$⊢ φ \to U = {Base}_{C}$

Proof

Step	Hyp	Ref	Expression
1		setcbas.c	$⊢ C = SetCat (U)$
2		setcbas.u	$⊢ φ \to U \in V$
3		catstr	$⊢ \{⟨{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))⟩\} Struct ⟨1, 15⟩$
4		baseid	$⊢ Base = Slot {Base}_{ndx}$
5		snsstp1	$⊢ \{⟨{Base}_{ndx}, U⟩\} \subseteq \{⟨{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	3 4 5	strfv	$⊢ U \in V \to U = {Base}_{\{⟨{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))⟩\}}$
7	2 6	syl	$⊢ φ \to U = {Base}_{\{⟨{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))⟩\}}$
8		eqidd	$⊢ φ \to (x \in U, y \in U ⟼ y^{x}) = (x \in U, y \in U ⟼ y^{x})$
9		eqidd	$⊢ φ \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))$
10	1 2 8 9	setcval	$⊢ φ \to C = \{⟨{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))⟩\}$
11	10	fveq2d	$⊢ φ \to {Base}_{C} = {Base}_{\{⟨{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))⟩\}}$
12	7 11	eqtr4d	$⊢ φ \to U = {Base}_{C}$