fuccofval

Description: Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucval.q	$⊢ Q = C FuncCat D$
	fucval.b	$⊢ B = C Func D$
	fucval.n	$⊢ N = C Nat D$
	fucval.a	$⊢ A = {Base}_{C}$
	fucval.o	$⊢ \underset{˙}{\cdot} = comp (D)$
	fucval.c	$⊢ φ \to C \in Cat$
	fucval.d	$⊢ φ \to D \in Cat$
	fuccofval.x	$⊢ \underset{˙}{∙} = comp (Q)$
Assertion	fuccofval	$⊢ φ \to \underset{˙}{∙} = (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))$

Proof

Step	Hyp	Ref	Expression
1		fucval.q	$⊢ Q = C FuncCat D$
2		fucval.b	$⊢ B = C Func D$
3		fucval.n	$⊢ N = C Nat D$
4		fucval.a	$⊢ A = {Base}_{C}$
5		fucval.o	$⊢ \underset{˙}{\cdot} = comp (D)$
6		fucval.c	$⊢ φ \to C \in Cat$
7		fucval.d	$⊢ φ \to D \in Cat$
8		fuccofval.x	$⊢ \underset{˙}{∙} = comp (Q)$
9		eqidd	$⊢ φ \to (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x)))) = (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))$
10	1 2 3 4 5 6 7 9	fucval	$⊢ φ \to Q = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))⟩\}$
11	10	fveq2d	$⊢ φ \to comp (Q) = comp (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))⟩\})$
12	2	ovexi	$⊢ B \in V$
13	12 12	xpex	$⊢ B \times B \in V$
14	13 12	mpoex	$⊢ (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x)))) \in V$
15		catstr	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))⟩\} Struct ⟨1, 15⟩$
16		ccoid	$⊢ comp = Slot comp (ndx)$
17		snsstp3	$⊢ \{⟨comp (ndx), (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))⟩\}$
18	15 16 17	strfv	$⊢ (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x)))) \in V \to (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x)))) = comp (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))⟩\})$
19	14 18	ax-mp	$⊢ (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x)))) = comp (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))⟩\})$
20	11 8 19	3eqtr4g	$⊢ φ \to \underset{˙}{∙} = (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))$

Metamath Proof Explorer

Theorem fuccofval

Proof