Metamath Proof Explorer

Theorem 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 ∈ Cat ∧ D ∈ Cat → C ∈ Cat
7 simpr ⊢ C ∈ Cat ∧ D ∈ Cat → D ∈ Cat
8 eqid ⊢ comp ⁡ Q = comp ⁡ Q
9 1 2 3 4 5 6 7 8 fuccofval ⊢ C ∈ Cat ∧ D ∈ Cat → comp ⁡ Q = v ∈ C Func D × C Func D , h ∈ C Func D ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g C Nat D h , a ∈ f C Nat D g ⟼ x ∈ 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 ∈ Cat ∧ D ∈ Cat → 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 ⊆ Base ndx C Func D Hom ⁡ ndx C Nat D comp ⁡ ndx comp ⁡ Q
14 ovexd ⊢ C ∈ Cat ∧ D ∈ Cat → C Func D ∈ V
15 eqid ⊢ Base Q = Base Q
16 10 11 12 13 14 15 strfv3 ⊢ C ∈ Cat ∧ D ∈ Cat → Base Q = C Func D
17 16 eqcomd ⊢ C ∈ Cat ∧ D ∈ Cat → C Func D = Base Q
18 base0 ⊢ ∅ = Base ∅
19 funcrcl ⊢ f ∈ C Func D → C ∈ Cat ∧ D ∈ Cat
20 19 con3i ⊢ ¬ C ∈ Cat ∧ D ∈ Cat → ¬ f ∈ C Func D
21 20 eq0rdv ⊢ ¬ C ∈ Cat ∧ D ∈ Cat → C Func D = ∅
22 fnfuc ⊢ FuncCat Fn Cat × Cat
23 fndm ⊢ FuncCat Fn Cat × Cat → dom ⁡ FuncCat = Cat × Cat
24 22 23 ax-mp ⊢ dom ⁡ FuncCat = Cat × Cat
25 24 ndmov ⊢ ¬ C ∈ Cat ∧ D ∈ Cat → C FuncCat D = ∅
26 1 25 syl5eq ⊢ ¬ C ∈ Cat ∧ D ∈ Cat → Q = ∅
27 26 fveq2d ⊢ ¬ C ∈ Cat ∧ D ∈ Cat → Base Q = Base ∅
28 18 21 27 3eqtr4a ⊢ ¬ C ∈ Cat ∧ D ∈ Cat → C Func D = Base Q
29 17 28 pm2.61i ⊢ C Func D = Base Q