fuchom

Description: The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucbas.q	$⊢ Q = C FuncCat D$
	fuchom.n	$⊢ N = C Nat D$
Assertion	fuchom	$⊢ N = Hom (Q)$

Proof

Step	Hyp	Ref	Expression
1		fucbas.q	$⊢ Q = C FuncCat D$
2		fuchom.n	$⊢ N = C Nat D$
3		eqid	$⊢ C Func D = C Func D$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5		eqid	$⊢ comp (D) = comp (D)$
6		simpl	$⊢ (C \in Cat \land D \in Cat) \to C \in Cat$
7		simpr	$⊢ (C \in Cat \land D \in Cat) \to D \in Cat$
8		eqid	$⊢ comp (Q) = comp (Q)$
9	1 3 2 4 5 6 7 8	fuccofval	$⊢ (C \in Cat \land D \in Cat) \to comp (Q) = (v \in ((C Func D) \times (C Func D)), h \in (C Func D) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in {Base}_{C} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))))$
10	1 3 2 4 5 6 7 9	fucval	$⊢ (C \in Cat \land D \in Cat) \to Q = \{⟨{Base}_{ndx}, C Func D⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), comp (Q)⟩\}$
11		catstr	$⊢ \{⟨{Base}_{ndx}, C Func D⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), comp (Q)⟩\} Struct ⟨1, 15⟩$
12		homid	$⊢ Hom = Slot Hom (ndx)$
13		snsstp2	$⊢ \{⟨Hom (ndx), N⟩\} \subseteq \{⟨{Base}_{ndx}, C Func D⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), comp (Q)⟩\}$
14	2	ovexi	$⊢ N \in V$
15	14	a1i	$⊢ (C \in Cat \land D \in Cat) \to N \in V$
16		eqid	$⊢ Hom (Q) = Hom (Q)$
17	10 11 12 13 15 16	strfv3	$⊢ (C \in Cat \land D \in Cat) \to Hom (Q) = N$
18	17	eqcomd	$⊢ (C \in Cat \land D \in Cat) \to N = Hom (Q)$
19		df-hom	$⊢ Hom = Slot 14$
20	19	str0	$⊢ \emptyset = Hom (\emptyset)$
21	2	natffn	$⊢ N Fn ((C Func D) \times (C Func D))$
22		funcrcl	$⊢ f \in (C Func D) \to (C \in Cat \land D \in Cat)$
23	22	con3i	$⊢ \neg (C \in Cat \land D \in Cat) \to \neg f \in (C Func D)$
24	23	eq0rdv	$⊢ \neg (C \in Cat \land D \in Cat) \to C Func D = \emptyset$
25	24	xpeq2d	$⊢ \neg (C \in Cat \land D \in Cat) \to (C Func D) \times (C Func D) = (C Func D) \times \emptyset$
26		xp0	$⊢ (C Func D) \times \emptyset = \emptyset$
27	25 26	eqtrdi	$⊢ \neg (C \in Cat \land D \in Cat) \to (C Func D) \times (C Func D) = \emptyset$
28	27	fneq2d	$⊢ \neg (C \in Cat \land D \in Cat) \to (N Fn ((C Func D) \times (C Func D)) \leftrightarrow N Fn \emptyset)$
29	21 28	mpbii	$⊢ \neg (C \in Cat \land D \in Cat) \to N Fn \emptyset$
30		fn0	$⊢ N Fn \emptyset \leftrightarrow N = \emptyset$
31	29 30	sylib	$⊢ \neg (C \in Cat \land D \in Cat) \to N = \emptyset$
32		fnfuc	$⊢ FuncCat Fn (Cat \times Cat)$
33	32	fndmi	$⊢ dom FuncCat = Cat \times Cat$
34	33	ndmov	$⊢ \neg (C \in Cat \land D \in Cat) \to C FuncCat D = \emptyset$
35	1 34	syl5eq	$⊢ \neg (C \in Cat \land D \in Cat) \to Q = \emptyset$
36	35	fveq2d	$⊢ \neg (C \in Cat \land D \in Cat) \to Hom (Q) = Hom (\emptyset)$
37	20 31 36	3eqtr4a	$⊢ \neg (C \in Cat \land D \in Cat) \to N = Hom (Q)$
38	18 37	pm2.61i	$⊢ N = Hom (Q)$

Metamath Proof Explorer

Theorem fuchom

Proof