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 e. Cat -> ( Homf ` C ) e. ( Subcat ` C ) )

Proof

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