fuccoval

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

	Ref	Expression
Hypotheses	fucco.q	$⊢ Q = C FuncCat D$
	fucco.n	$⊢ N = C Nat D$
	fucco.a	$⊢ A = {Base}_{C}$
	fucco.o	$⊢ \underset{˙}{\cdot} = comp (D)$
	fucco.x	$⊢ \underset{˙}{∙} = comp (Q)$
	fucco.f	$⊢ φ \to R \in (F N G)$
	fucco.g	$⊢ φ \to S \in (G N H)$
	fuccoval.f	$⊢ φ \to X \in A$
Assertion	fuccoval	$⊢ φ \to (S (⟨F, G⟩ \underset{˙}{∙} H) R) (X) = S (X) (⟨1^{st} (F) (X), 1^{st} (G) (X)⟩ \underset{˙}{\cdot} 1^{st} (H) (X)) R (X)$

Proof

Step	Hyp	Ref	Expression
1		fucco.q	$⊢ Q = C FuncCat D$
2		fucco.n	$⊢ N = C Nat D$
3		fucco.a	$⊢ A = {Base}_{C}$
4		fucco.o	$⊢ \underset{˙}{\cdot} = comp (D)$
5		fucco.x	$⊢ \underset{˙}{∙} = comp (Q)$
6		fucco.f	$⊢ φ \to R \in (F N G)$
7		fucco.g	$⊢ φ \to S \in (G N H)$
8		fuccoval.f	$⊢ φ \to X \in A$
9	1 2 3 4 5 6 7	fucco	$⊢ φ \to S (⟨F, G⟩ \underset{˙}{∙} H) R = (x \in A ⟼ S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) R (x))$
10		simpr	$⊢ (φ \land x = X) \to x = X$
11	10	fveq2d	$⊢ (φ \land x = X) \to 1^{st} (F) (x) = 1^{st} (F) (X)$
12	10	fveq2d	$⊢ (φ \land x = X) \to 1^{st} (G) (x) = 1^{st} (G) (X)$
13	11 12	opeq12d	$⊢ (φ \land x = X) \to ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ = ⟨1^{st} (F) (X), 1^{st} (G) (X)⟩$
14	10	fveq2d	$⊢ (φ \land x = X) \to 1^{st} (H) (x) = 1^{st} (H) (X)$
15	13 14	oveq12d	$⊢ (φ \land x = X) \to ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x) = ⟨1^{st} (F) (X), 1^{st} (G) (X)⟩ \underset{˙}{\cdot} 1^{st} (H) (X)$
16	10	fveq2d	$⊢ (φ \land x = X) \to S (x) = S (X)$
17	10	fveq2d	$⊢ (φ \land x = X) \to R (x) = R (X)$
18	15 16 17	oveq123d	$⊢ (φ \land x = X) \to S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) R (x) = S (X) (⟨1^{st} (F) (X), 1^{st} (G) (X)⟩ \underset{˙}{\cdot} 1^{st} (H) (X)) R (X)$
19		ovexd	$⊢ φ \to S (X) (⟨1^{st} (F) (X), 1^{st} (G) (X)⟩ \underset{˙}{\cdot} 1^{st} (H) (X)) R (X) \in V$
20	9 18 8 19	fvmptd	$⊢ φ \to (S (⟨F, G⟩ \underset{˙}{∙} H) R) (X) = S (X) (⟨1^{st} (F) (X), 1^{st} (G) (X)⟩ \underset{˙}{\cdot} 1^{st} (H) (X)) R (X)$

Metamath Proof Explorer

Theorem fuccoval

Proof