fuccatid

Description: The functor category is a category. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fuccat.q	$⊢ Q = C FuncCat D$
	fuccat.r	$⊢ φ \to C \in Cat$
	fuccat.s	$⊢ φ \to D \in Cat$
	fuccatid.1	$⊢ \underset{˙}{1} = Id (D)$
Assertion	fuccatid	$⊢ φ \to (Q \in Cat \land Id (Q) = (f \in (C Func D) ⟼ \underset{˙}{1} \circ 1^{st} (f)))$

Proof

Step	Hyp	Ref	Expression
1		fuccat.q	$⊢ Q = C FuncCat D$
2		fuccat.r	$⊢ φ \to C \in Cat$
3		fuccat.s	$⊢ φ \to D \in Cat$
4		fuccatid.1	$⊢ \underset{˙}{1} = Id (D)$
5	1	fucbas	$⊢ C Func D = {Base}_{Q}$
6	5	a1i	$⊢ φ \to C Func D = {Base}_{Q}$
7		eqid	$⊢ C Nat D = C Nat D$
8	1 7	fuchom	$⊢ C Nat D = Hom (Q)$
9	8	a1i	$⊢ φ \to C Nat D = Hom (Q)$
10		eqidd	$⊢ φ \to comp (Q) = comp (Q)$
11	1	ovexi	$⊢ Q \in V$
12	11	a1i	$⊢ φ \to Q \in V$
13		biid	$⊢ ((e \in (C Func D) \land f \in (C Func D)) \land (g \in (C Func D) \land h \in (C Func D)) \land (r \in (e (C Nat D) f) \land s \in (f (C Nat D) g) \land t \in (g (C Nat D) h))) \leftrightarrow ((e \in (C Func D) \land f \in (C Func D)) \land (g \in (C Func D) \land h \in (C Func D)) \land (r \in (e (C Nat D) f) \land s \in (f (C Nat D) g) \land t \in (g (C Nat D) h)))$
14		simpr	$⊢ (φ \land f \in (C Func D)) \to f \in (C Func D)$
15	1 7 4 14	fucidcl	$⊢ (φ \land f \in (C Func D)) \to \underset{˙}{1} \circ 1^{st} (f) \in (f (C Nat D) f)$
16		eqid	$⊢ comp (Q) = comp (Q)$
17		simpr31	$⊢ (φ \land ((e \in (C Func D) \land f \in (C Func D)) \land (g \in (C Func D) \land h \in (C Func D)) \land (r \in (e (C Nat D) f) \land s \in (f (C Nat D) g) \land t \in (g (C Nat D) h)))) \to r \in (e (C Nat D) f)$
18	1 7 16 4 17	fuclid	$⊢ (φ \land ((e \in (C Func D) \land f \in (C Func D)) \land (g \in (C Func D) \land h \in (C Func D)) \land (r \in (e (C Nat D) f) \land s \in (f (C Nat D) g) \land t \in (g (C Nat D) h)))) \to (\underset{˙}{1} \circ 1^{st} (f)) (⟨e, f⟩ comp (Q) f) r = r$
19		simpr32	$⊢ (φ \land ((e \in (C Func D) \land f \in (C Func D)) \land (g \in (C Func D) \land h \in (C Func D)) \land (r \in (e (C Nat D) f) \land s \in (f (C Nat D) g) \land t \in (g (C Nat D) h)))) \to s \in (f (C Nat D) g)$
20	1 7 16 4 19	fucrid	$⊢ (φ \land ((e \in (C Func D) \land f \in (C Func D)) \land (g \in (C Func D) \land h \in (C Func D)) \land (r \in (e (C Nat D) f) \land s \in (f (C Nat D) g) \land t \in (g (C Nat D) h)))) \to s (⟨f, f⟩ comp (Q) g) (\underset{˙}{1} \circ 1^{st} (f)) = s$
21	1 7 16 17 19	fuccocl	$⊢ (φ \land ((e \in (C Func D) \land f \in (C Func D)) \land (g \in (C Func D) \land h \in (C Func D)) \land (r \in (e (C Nat D) f) \land s \in (f (C Nat D) g) \land t \in (g (C Nat D) h)))) \to s (⟨e, f⟩ comp (Q) g) r \in (e (C Nat D) g)$
22		simpr33	$⊢ (φ \land ((e \in (C Func D) \land f \in (C Func D)) \land (g \in (C Func D) \land h \in (C Func D)) \land (r \in (e (C Nat D) f) \land s \in (f (C Nat D) g) \land t \in (g (C Nat D) h)))) \to t \in (g (C Nat D) h)$
23	1 7 16 17 19 22	fucass	$⊢ (φ \land ((e \in (C Func D) \land f \in (C Func D)) \land (g \in (C Func D) \land h \in (C Func D)) \land (r \in (e (C Nat D) f) \land s \in (f (C Nat D) g) \land t \in (g (C Nat D) h)))) \to (t (⟨f, g⟩ comp (Q) h) s) (⟨e, f⟩ comp (Q) h) r = t (⟨e, g⟩ comp (Q) h) (s (⟨e, f⟩ comp (Q) g) r)$
24	6 9 10 12 13 15 18 20 21 23	iscatd2	$⊢ φ \to (Q \in Cat \land Id (Q) = (f \in (C Func D) ⟼ \underset{˙}{1} \circ 1^{st} (f)))$

Metamath Proof Explorer

Theorem fuccatid

Proof