Metamath Proof Explorer

Theorem 0catg

Description: Any structure with an empty set of objects is a category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Assertion 0catg 
|- ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. Cat )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( C e. V /\ (/) = ( Base ` C ) ) -> (/) = ( Base ` C ) )
2 eqidd 
 |-  ( ( C e. V /\ (/) = ( Base ` C ) ) -> ( Hom ` C ) = ( Hom ` C ) )
3 eqidd 
 |-  ( ( C e. V /\ (/) = ( Base ` C ) ) -> ( comp ` C ) = ( comp ` C ) )
4 simpl 
 |-  ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. V )
5 noel 
 |-  -. x e. (/)
6 5 pm2.21i 
 |-  ( x e. (/) -> (/) e. ( x ( Hom ` C ) x ) )
7 6 adantl 
 |-  ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ x e. (/) ) -> (/) e. ( x ( Hom ` C ) x ) )
8 simpr1 
 |-  ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( x e. (/) /\ y e. (/) /\ f e. ( y ( Hom ` C ) x ) ) ) -> x e. (/) )
9 5 pm2.21i 
 |-  ( x e. (/) -> ( (/) ( <. y , x >. ( comp ` C ) x ) f ) = f )
10 8 9 syl 
 |-  ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( x e. (/) /\ y e. (/) /\ f e. ( y ( Hom ` C ) x ) ) ) -> ( (/) ( <. y , x >. ( comp ` C ) x ) f ) = f )
11 simpr1 
 |-  ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( x e. (/) /\ y e. (/) /\ f e. ( x ( Hom ` C ) y ) ) ) -> x e. (/) )
12 5 pm2.21i 
 |-  ( x e. (/) -> ( f ( <. x , x >. ( comp ` C ) y ) (/) ) = f )
13 11 12 syl 
 |-  ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( x e. (/) /\ y e. (/) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( f ( <. x , x >. ( comp ` C ) y ) (/) ) = f )
14 simp21 
 |-  ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( x e. (/) /\ y e. (/) /\ z e. (/) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> x e. (/) )
15 5 pm2.21i 
 |-  ( x e. (/) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) )
16 14 15 syl 
 |-  ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( x e. (/) /\ y e. (/) /\ z e. (/) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) )
17 simp2ll 
 |-  ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( ( x e. (/) /\ y e. (/) ) /\ ( z e. (/) /\ w e. (/) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ h e. ( z ( Hom ` C ) w ) ) ) -> x e. (/) )
18 5 pm2.21i 
 |-  ( x e. (/) -> ( ( h ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( h ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) )
19 17 18 syl 
 |-  ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( ( x e. (/) /\ y e. (/) ) /\ ( z e. (/) /\ w e. (/) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ h e. ( z ( Hom ` C ) w ) ) ) -> ( ( h ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( h ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) )
20 1 2 3 4 7 10 13 16 19 iscatd 
 |-  ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. Cat )