Theorem 0catg 16348

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

Assertion

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

Proof of Theorem 0catg

Dummy variables f g h w x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 477	. 2 |- ( ( C e. V /\ (/) = ( Base ` C ) ) -> (/) = ( Base ` C ) )
2		eqidd 2623	. 2 |- ( ( C e. V /\ (/) = ( Base ` C ) ) -> ( Hom ` C ) = ( Hom ` C ) )
3		eqidd 2623	. 2 |- ( ( C e. V /\ (/) = ( Base ` C ) ) -> (comp ` C ) = (comp ` C ) )
4		simpl 473	. 2 |- ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. V )
5		noel 3919	. . . 4 |- -. x e. (/)
6	5	pm2.21i 116	. . 3 |- ( x e. (/) -> (/) e. ( x ( Hom ` C ) x ) )
7	6	adantl 482	. 2 |- ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ x e. (/) ) -> (/) e. ( x ( Hom ` C ) x ) )
8		simpr1 1067	. . 3 |- ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( x e. (/) /\ y e. (/) /\ f e. ( y ( Hom ` C ) x ) ) ) -> x e. (/) )
9	5	pm2.21i 116	. . 3 |- ( x e. (/) -> ( (/) ( <. y , x >. (comp ` C ) x ) f ) = f )
10	8, 9	syl 17	. 2 |- ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( x e. (/) /\ y e. (/) /\ f e. ( y ( Hom ` C ) x ) ) ) -> ( (/) ( <. y , x >. (comp ` C ) x ) f ) = f )
11		simpr1 1067	. . 3 |- ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( x e. (/) /\ y e. (/) /\ f e. ( x ( Hom ` C ) y ) ) ) -> x e. (/) )
12	5	pm2.21i 116	. . 3 |- ( x e. (/) -> ( f ( <. x , x >. (comp ` C ) y ) (/) ) = f )
13	11, 12	syl 17	. 2 |- ( ( ( C e. V /\ (/) = ( Base ` C ) ) /\ ( x e. (/) /\ y e. (/) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( f ( <. x , x >. (comp ` C ) y ) (/) ) = f )
14		simp21 1094	. . 3 |- ( ( ( 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 116	. . 3 |- ( x e. (/) -> ( g ( <. x , y >. (comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) )
16	14, 15	syl 17	. 2 |- ( ( ( 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 1128	. . 3 |- ( ( ( 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 116	. . 3 |- ( 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 17	. 2 |- ( ( ( 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 16334	1 |- ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. Cat )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   (/)c0 3915   <.cop 4183   ` cfv 5888  (class class class)co 6650   Basecbs 15857   Hom chom 15952  compcco 15953   Catccat 16325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-cat 16329

This theorem is referenced by:  0cat  16349