Metamath Proof Explorer

Theorem incat

Description: Constructing a category with at most one object and at most two morphisms. If X is a set then C is the category A in Exercise 3G of Adamek p. 45. (Contributed by Zhi Wang, 5-Nov-2025)

Ref Expression
Hypotheses incat.c 
|- C = { <. ( Base ` ndx ) , { X } >. , <. ( Hom ` ndx ) , { <. X , X , H >. } >. , <. ( comp ` ndx ) , { <. <. X , X >. , X , .x. >. } >. }
incat.h 
|- H = { F , G }
incat.x 
|- .x. = ( f e. H , g e. H |-> ( f i^i g ) )
Assertion incat 
|- ( ( F C_ G /\ G e. V ) -> ( C e. Cat /\ ( Id ` C ) = ( y e. { X } |-> G ) ) )

Proof

Step Hyp Ref Expression
1 incat.c 
 |-  C = { <. ( Base ` ndx ) , { X } >. , <. ( Hom ` ndx ) , { <. X , X , H >. } >. , <. ( comp ` ndx ) , { <. <. X , X >. , X , .x. >. } >. }
2 incat.h 
 |-  H = { F , G }
3 incat.x 
 |-  .x. = ( f e. H , g e. H |-> ( f i^i g ) )
4 snex 
 |-  { X } e. _V
5 1 4 catbas 
 |-  { X } = ( Base ` C )
6 5 a1i 
 |-  ( ( F C_ G /\ G e. V ) -> { X } = ( Base ` C ) )
7 snex 
 |-  { <. X , X , H >. } e. _V
8 1 7 cathomfval 
 |-  { <. X , X , H >. } = ( Hom ` C )
9 8 a1i 
 |-  ( ( F C_ G /\ G e. V ) -> { <. X , X , H >. } = ( Hom ` C ) )
10 snex 
 |-  { <. <. X , X >. , X , .x. >. } e. _V
11 1 10 catcofval 
 |-  { <. <. X , X >. , X , .x. >. } = ( comp ` C )
12 11 a1i 
 |-  ( ( F C_ G /\ G e. V ) -> { <. <. X , X >. , X , .x. >. } = ( comp ` C ) )
13 prex 
 |-  { F , G } e. _V
14 2 13 eqeltri 
 |-  H e. _V
15 14 ovsn2 
 |-  ( X { <. X , X , H >. } X ) = H
16 15 2 eqtri 
 |-  ( X { <. X , X , H >. } X ) = { F , G }
17 14 14 mpoex 
 |-  ( f e. H , g e. H |-> ( f i^i g ) ) e. _V
18 3 17 eqeltri 
 |-  .x. e. _V
19 18 ovsn2 
 |-  ( <. X , X >. { <. <. X , X >. , X , .x. >. } X ) = .x.
20 19 3 eqtri 
 |-  ( <. X , X >. { <. <. X , X >. , X , .x. >. } X ) = ( f e. H , g e. H |-> ( f i^i g ) )
21 20 a1i 
 |-  ( ( F C_ G /\ G e. V ) -> ( <. X , X >. { <. <. X , X >. , X , .x. >. } X ) = ( f e. H , g e. H |-> ( f i^i g ) ) )
22 ineq12 
 |-  ( ( f = G /\ g = G ) -> ( f i^i g ) = ( G i^i G ) )
23 inidm 
 |-  ( G i^i G ) = G
24 22 23 eqtrdi 
 |-  ( ( f = G /\ g = G ) -> ( f i^i g ) = G )
25 24 adantl 
 |-  ( ( ( F C_ G /\ G e. V ) /\ ( f = G /\ g = G ) ) -> ( f i^i g ) = G )
26 prid2g 
 |-  ( G e. V -> G e. { F , G } )
27 26 2 eleqtrrdi 
 |-  ( G e. V -> G e. H )
28 27 adantl 
 |-  ( ( F C_ G /\ G e. V ) -> G e. H )
29 21 25 28 28 28 ovmpod 
 |-  ( ( F C_ G /\ G e. V ) -> ( G ( <. X , X >. { <. <. X , X >. , X , .x. >. } X ) G ) = G )
30 ineq12 
 |-  ( ( f = G /\ g = F ) -> ( f i^i g ) = ( G i^i F ) )
31 sseqin2 
 |-  ( F C_ G <-> ( G i^i F ) = F )
32 31 biimpi 
 |-  ( F C_ G -> ( G i^i F ) = F )
33 32 adantr 
 |-  ( ( F C_ G /\ G e. V ) -> ( G i^i F ) = F )
34 30 33 sylan9eqr 
 |-  ( ( ( F C_ G /\ G e. V ) /\ ( f = G /\ g = F ) ) -> ( f i^i g ) = F )
35 ssexg 
 |-  ( ( F C_ G /\ G e. V ) -> F e. _V )
36 prid1g 
 |-  ( F e. _V -> F e. { F , G } )
37 35 36 syl 
 |-  ( ( F C_ G /\ G e. V ) -> F e. { F , G } )
38 37 2 eleqtrrdi 
 |-  ( ( F C_ G /\ G e. V ) -> F e. H )
39 21 34 28 38 38 ovmpod 
 |-  ( ( F C_ G /\ G e. V ) -> ( G ( <. X , X >. { <. <. X , X >. , X , .x. >. } X ) F ) = F )
40 ineq12 
 |-  ( ( f = F /\ g = G ) -> ( f i^i g ) = ( F i^i G ) )
41 dfss2 
 |-  ( F C_ G <-> ( F i^i G ) = F )
42 41 biimpi 
 |-  ( F C_ G -> ( F i^i G ) = F )
43 42 adantr 
 |-  ( ( F C_ G /\ G e. V ) -> ( F i^i G ) = F )
44 40 43 sylan9eqr 
 |-  ( ( ( F C_ G /\ G e. V ) /\ ( f = F /\ g = G ) ) -> ( f i^i g ) = F )
45 21 44 38 28 38 ovmpod 
 |-  ( ( F C_ G /\ G e. V ) -> ( F ( <. X , X >. { <. <. X , X >. , X , .x. >. } X ) G ) = F )
46 ineq12 
 |-  ( ( f = F /\ g = F ) -> ( f i^i g ) = ( F i^i F ) )
47 inidm 
 |-  ( F i^i F ) = F
48 46 47 eqtrdi 
 |-  ( ( f = F /\ g = F ) -> ( f i^i g ) = F )
49 48 adantl 
 |-  ( ( ( F C_ G /\ G e. V ) /\ ( f = F /\ g = F ) ) -> ( f i^i g ) = F )
50 21 49 38 38 38 ovmpod 
 |-  ( ( F C_ G /\ G e. V ) -> ( F ( <. X , X >. { <. <. X , X >. , X , .x. >. } X ) F ) = F )
51 50 37 eqeltrd 
 |-  ( ( F C_ G /\ G e. V ) -> ( F ( <. X , X >. { <. <. X , X >. , X , .x. >. } X ) F ) e. { F , G } )
52 6 9 12 16 29 39 45 51 2arwcat 
 |-  ( ( F C_ G /\ G e. V ) -> ( C e. Cat /\ ( Id ` C ) = ( y e. { X } |-> G ) ) )