fucbas

Description: The objects of the functor category are functors from C to D . (Contributed by Mario Carneiro, 6-Jan-2017) (Revised by Mario Carneiro, 12-Jan-2017)

		Ref	Expression
	Hypothesis	fucbas.q	$⊢ Q = C FuncCat D$
	Assertion	fucbas	$⊢ C Func D = {Base}_{Q}$

Proof

Step	Hyp	Ref	Expression
1		fucbas.q	$⊢ Q = C FuncCat D$
2		eqid	$⊢ C Func D = C Func D$
3		eqid	$⊢ C Nat D = C Nat 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 2 3 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 (C Nat D) h), a \in (f (C Nat D) 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 2 3 4 5 6 7 9	fucval	$⊢ (C \in Cat \land D \in Cat) \to Q = \{⟨{Base}_{ndx}, C Func D⟩, ⟨Hom (ndx), C Nat D⟩, ⟨comp (ndx), comp (Q)⟩\}$
11		catstr	$⊢ \{⟨{Base}_{ndx}, C Func D⟩, ⟨Hom (ndx), C Nat D⟩, ⟨comp (ndx), comp (Q)⟩\} Struct ⟨1, 15⟩$
12		baseid	$⊢ Base = Slot {Base}_{ndx}$
13		snsstp1	$⊢ \{⟨{Base}_{ndx}, C Func D⟩\} \subseteq \{⟨{Base}_{ndx}, C Func D⟩, ⟨Hom (ndx), C Nat D⟩, ⟨comp (ndx), comp (Q)⟩\}$
14		ovexd	$⊢ (C \in Cat \land D \in Cat) \to C Func D \in V$
15		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
16	10 11 12 13 14 15	strfv3	$⊢ (C \in Cat \land D \in Cat) \to {Base}_{Q} = C Func D$
17	16	eqcomd	$⊢ (C \in Cat \land D \in Cat) \to C Func D = {Base}_{Q}$
18		base0	$⊢ \emptyset = {Base}_{\emptyset}$
19		funcrcl	$⊢ f \in (C Func D) \to (C \in Cat \land D \in Cat)$
20	19	con3i	$⊢ \neg (C \in Cat \land D \in Cat) \to \neg f \in (C Func D)$
21	20	eq0rdv	$⊢ \neg (C \in Cat \land D \in Cat) \to C Func D = \emptyset$
22		fnfuc	$⊢ FuncCat Fn (Cat \times Cat)$
23	22	fndmi	$⊢ dom FuncCat = Cat \times Cat$
24	23	ndmov	$⊢ \neg (C \in Cat \land D \in Cat) \to C FuncCat D = \emptyset$
25	1 24	eqtrid	$⊢ \neg (C \in Cat \land D \in Cat) \to Q = \emptyset$
26	25	fveq2d	$⊢ \neg (C \in Cat \land D \in Cat) \to {Base}_{Q} = {Base}_{\emptyset}$
27	18 21 26	3eqtr4a	$⊢ \neg (C \in Cat \land D \in Cat) \to C Func D = {Base}_{Q}$
28	17 27	pm2.61i	$⊢ C Func D = {Base}_{Q}$

Metamath Proof Explorer

Theorem fucbas

Proof