Metamath Proof Explorer

Theorem catcbas

Description: Set of objects of the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017)

		Ref	Expression
	Hypotheses	catcbas.c	$⊢ C = CatCat (U)$
		catcbas.b	$⊢ B = {Base}_{C}$
		catcbas.u	$⊢ φ \to U \in V$
	Assertion	catcbas	$⊢ φ \to B = U \cap Cat$

Proof

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