Metamath Proof Explorer


Theorem catsubcat

Description: For any category C , C itself is a (full) subcategory of C , see example 4.3(1.b) in Adamek p. 48. (Contributed by AV, 23-Apr-2020)

Ref Expression
Assertion catsubcat C Cat Hom 𝑓 C Subcat C

Proof

Step Hyp Ref Expression
1 ssidd C Cat Base C Base C
2 ssidd C Cat x Base C y Base C x Hom 𝑓 C y x Hom 𝑓 C y
3 2 ralrimivva C Cat x Base C y Base C x Hom 𝑓 C y x Hom 𝑓 C y
4 eqid Hom 𝑓 C = Hom 𝑓 C
5 eqid Base C = Base C
6 4 5 homffn Hom 𝑓 C Fn Base C × Base C
7 6 a1i C Cat Hom 𝑓 C Fn Base C × Base C
8 fvexd C Cat Base C V
9 7 7 8 isssc C Cat Hom 𝑓 C cat Hom 𝑓 C Base C Base C x Base C y Base C x Hom 𝑓 C y x Hom 𝑓 C y
10 1 3 9 mpbir2and C Cat Hom 𝑓 C cat Hom 𝑓 C
11 eqid Hom C = Hom C
12 eqid Id C = Id C
13 simpl C Cat x Base C C Cat
14 simpr C Cat x Base C x Base C
15 5 11 12 13 14 catidcl C Cat x Base C Id C x x Hom C x
16 4 5 11 14 14 homfval C Cat x Base C x Hom 𝑓 C x = x Hom C x
17 15 16 eleqtrrd C Cat x Base C Id C x x Hom 𝑓 C x
18 eqid comp C = comp C
19 13 adantr C Cat x Base C y Base C z Base C C Cat
20 19 adantr C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z C Cat
21 14 adantr C Cat x Base C y Base C z Base C x Base C
22 21 adantr C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z x Base C
23 simpl y Base C z Base C y Base C
24 23 adantl C Cat x Base C y Base C z Base C y Base C
25 24 adantr C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z y Base C
26 simpr y Base C z Base C z Base C
27 26 adantl C Cat x Base C y Base C z Base C z Base C
28 27 adantr C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z z Base C
29 4 5 11 21 24 homfval C Cat x Base C y Base C z Base C x Hom 𝑓 C y = x Hom C y
30 29 eleq2d C Cat x Base C y Base C z Base C f x Hom 𝑓 C y f x Hom C y
31 30 biimpcd f x Hom 𝑓 C y C Cat x Base C y Base C z Base C f x Hom C y
32 31 adantr f x Hom 𝑓 C y g y Hom 𝑓 C z C Cat x Base C y Base C z Base C f x Hom C y
33 32 impcom C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z f x Hom C y
34 4 5 11 24 27 homfval C Cat x Base C y Base C z Base C y Hom 𝑓 C z = y Hom C z
35 34 eleq2d C Cat x Base C y Base C z Base C g y Hom 𝑓 C z g y Hom C z
36 35 biimpd C Cat x Base C y Base C z Base C g y Hom 𝑓 C z g y Hom C z
37 36 adantld C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z g y Hom C z
38 37 imp C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z g y Hom C z
39 5 11 18 20 22 25 28 33 38 catcocl C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z g x y comp C z f x Hom C z
40 4 5 11 21 27 homfval C Cat x Base C y Base C z Base C x Hom 𝑓 C z = x Hom C z
41 40 adantr C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z x Hom 𝑓 C z = x Hom C z
42 39 41 eleqtrrd C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z g x y comp C z f x Hom 𝑓 C z
43 42 ralrimivva C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z g x y comp C z f x Hom 𝑓 C z
44 43 ralrimivva C Cat x Base C y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z g x y comp C z f x Hom 𝑓 C z
45 17 44 jca C Cat x Base C Id C x x Hom 𝑓 C x y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z g x y comp C z f x Hom 𝑓 C z
46 45 ralrimiva C Cat x Base C Id C x x Hom 𝑓 C x y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z g x y comp C z f x Hom 𝑓 C z
47 id C Cat C Cat
48 4 12 18 47 7 issubc2 C Cat Hom 𝑓 C Subcat C Hom 𝑓 C cat Hom 𝑓 C x Base C Id C x x Hom 𝑓 C x y Base C z Base C f x Hom 𝑓 C y g y Hom 𝑓 C z g x y comp C z f x Hom 𝑓 C z
49 10 46 48 mpbir2and C Cat Hom 𝑓 C Subcat C