fuchom

Description: The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 14-Oct-2024)

	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	12	str0	$⊢ \emptyset = Hom (\emptyset)$
20	2	natffn	$⊢ N Fn ((C Func D) \times (C Func D))$
21		funcrcl	$⊢ f \in (C Func D) \to (C \in Cat \land D \in Cat)$
22	21	con3i	$⊢ \neg (C \in Cat \land D \in Cat) \to \neg f \in (C Func D)$
23	22	eq0rdv	$⊢ \neg (C \in Cat \land D \in Cat) \to C Func D = \emptyset$
24	23	xpeq2d	$⊢ \neg (C \in Cat \land D \in Cat) \to (C Func D) \times (C Func D) = (C Func D) \times \emptyset$
25		xp0	$⊢ (C Func D) \times \emptyset = \emptyset$
26	24 25	eqtrdi	$⊢ \neg (C \in Cat \land D \in Cat) \to (C Func D) \times (C Func D) = \emptyset$
27	26	fneq2d	$⊢ \neg (C \in Cat \land D \in Cat) \to (N Fn ((C Func D) \times (C Func D)) \leftrightarrow N Fn \emptyset)$
28	20 27	mpbii	$⊢ \neg (C \in Cat \land D \in Cat) \to N Fn \emptyset$
29		fn0	$⊢ N Fn \emptyset \leftrightarrow N = \emptyset$
30	28 29	sylib	$⊢ \neg (C \in Cat \land D \in Cat) \to N = \emptyset$
31		fnfuc	$⊢ FuncCat Fn (Cat \times Cat)$
32	31	fndmi	$⊢ dom FuncCat = Cat \times Cat$
33	32	ndmov	$⊢ \neg (C \in Cat \land D \in Cat) \to C FuncCat D = \emptyset$
34	1 33	syl5eq	$⊢ \neg (C \in Cat \land D \in Cat) \to Q = \emptyset$
35	34	fveq2d	$⊢ \neg (C \in Cat \land D \in Cat) \to Hom (Q) = Hom (\emptyset)$
36	19 30 35	3eqtr4a	$⊢ \neg (C \in Cat \land D \in Cat) \to N = Hom (Q)$
37	18 36	pm2.61i	$⊢ N = Hom (Q)$

Metamath Proof Explorer

Theorem fuchom

Proof