Metamath Proof Explorer

Theorem catchomfval

Description: Set of arrows of the category of categories (in a universe). (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$
		catchomfval.h	$⊢ H = Hom (C)$
	Assertion	catchomfval	$⊢ φ \to H = (x \in B, y \in B ⟼ x Func y)$

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		catchomfval.h	$⊢ H = Hom (C)$
5	1 2 3	catcbas	$⊢ φ \to B = U \cap Cat$
6		eqidd	$⊢ φ \to (x \in B, y \in B ⟼ x Func y) = (x \in B, y \in B ⟼ x Func y)$
7		eqidd	$⊢ φ \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))$
8	1 3 5 6 7	catcval	$⊢ φ \to C = \{⟨{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))⟩\}$
9	8	fveq2d	$⊢ φ \to Hom (C) = Hom (\{⟨{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))⟩\})$
10	4 9	syl5eq	$⊢ φ \to H = Hom (\{⟨{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))⟩\})$
11	2	fvexi	$⊢ B \in V$
12	11 11	mpoex	$⊢ (x \in B, y \in B ⟼ x Func y) \in V$
13		catstr	$⊢ \{⟨{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))⟩\} Struct ⟨1, 15⟩$
14		homid	$⊢ Hom = Slot Hom (ndx)$
15		snsstp2	$⊢ \{⟨Hom (ndx), (x \in B, y \in B ⟼ x Func y)⟩\} \subseteq \{⟨{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))⟩\}$
16	13 14 15	strfv	$⊢ (x \in B, y \in B ⟼ x Func y) \in V \to (x \in B, y \in B ⟼ x Func y) = Hom (\{⟨{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))⟩\})$
17	12 16	mp1i	$⊢ φ \to (x \in B, y \in B ⟼ x Func y) = Hom (\{⟨{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))⟩\})$
18	10 17	eqtr4d	$⊢ φ \to H = (x \in B, y \in B ⟼ x Func y)$