Metamath Proof Explorer

Theorem initc

Description: Sets with empty base are the only initial objects in the category of small categories. Example 7.2(3) of Adamek p. 101. (Contributed by Zhi Wang, 15-Nov-2025)

Ref Expression
Assertion initc 
|- ( ( C e. _V /\ (/) = ( Base ` C ) ) <-> A. d e. Cat E! f f e. ( C Func d ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( C e. _V /\ (/) = ( Base ` C ) ) /\ d e. Cat ) -> C e. _V )
2 simplr 
 |-  ( ( ( C e. _V /\ (/) = ( Base ` C ) ) /\ d e. Cat ) -> (/) = ( Base ` C ) )
3 simpr 
 |-  ( ( ( C e. _V /\ (/) = ( Base ` C ) ) /\ d e. Cat ) -> d e. Cat )
4 1 2 3 0funcg 
 |-  ( ( ( C e. _V /\ (/) = ( Base ` C ) ) /\ d e. Cat ) -> ( C Func d ) = { <. (/) , (/) >. } )
5 opex 
 |-  <. (/) , (/) >. e. _V
6 sneq 
 |-  ( f = <. (/) , (/) >. -> { f } = { <. (/) , (/) >. } )
7 6 eqeq2d 
 |-  ( f = <. (/) , (/) >. -> ( ( C Func d ) = { f } <-> ( C Func d ) = { <. (/) , (/) >. } ) )
8 5 7 spcev 
 |-  ( ( C Func d ) = { <. (/) , (/) >. } -> E. f ( C Func d ) = { f } )
9 4 8 syl 
 |-  ( ( ( C e. _V /\ (/) = ( Base ` C ) ) /\ d e. Cat ) -> E. f ( C Func d ) = { f } )
10 eusn 
 |-  ( E! f f e. ( C Func d ) <-> E. f ( C Func d ) = { f } )
11 9 10 sylibr 
 |-  ( ( ( C e. _V /\ (/) = ( Base ` C ) ) /\ d e. Cat ) -> E! f f e. ( C Func d ) )
12 11 ralrimiva 
 |-  ( ( C e. _V /\ (/) = ( Base ` C ) ) -> A. d e. Cat E! f f e. ( C Func d ) )
13 0cat 
 |-  (/) e. Cat
14 oveq2 
 |-  ( d = (/) -> ( C Func d ) = ( C Func (/) ) )
15 14 eleq2d 
 |-  ( d = (/) -> ( f e. ( C Func d ) <-> f e. ( C Func (/) ) ) )
16 15 eubidv 
 |-  ( d = (/) -> ( E! f f e. ( C Func d ) <-> E! f f e. ( C Func (/) ) ) )
17 16 rspcv 
 |-  ( (/) e. Cat -> ( A. d e. Cat E! f f e. ( C Func d ) -> E! f f e. ( C Func (/) ) ) )
18 13 17 ax-mp 
 |-  ( A. d e. Cat E! f f e. ( C Func d ) -> E! f f e. ( C Func (/) ) )
19 euex 
 |-  ( E! f f e. ( C Func (/) ) -> E. f f e. ( C Func (/) ) )
20 funcrcl 
 |-  ( f e. ( C Func (/) ) -> ( C e. Cat /\ (/) e. Cat ) )
21 20 simpld 
 |-  ( f e. ( C Func (/) ) -> C e. Cat )
22 21 elexd 
 |-  ( f e. ( C Func (/) ) -> C e. _V )
23 eqid 
 |-  ( Base ` C ) = ( Base ` C )
24 base0 
 |-  (/) = ( Base ` (/) )
25 eqidd 
 |-  ( f e. ( C Func (/) ) -> (/) = (/) )
26 id 
 |-  ( f e. ( C Func (/) ) -> f e. ( C Func (/) ) )
27 23 24 25 26 func0g2 
 |-  ( f e. ( C Func (/) ) -> ( Base ` C ) = (/) )
28 27 eqcomd 
 |-  ( f e. ( C Func (/) ) -> (/) = ( Base ` C ) )
29 22 28 jca 
 |-  ( f e. ( C Func (/) ) -> ( C e. _V /\ (/) = ( Base ` C ) ) )
30 29 exlimiv 
 |-  ( E. f f e. ( C Func (/) ) -> ( C e. _V /\ (/) = ( Base ` C ) ) )
31 18 19 30 3syl 
 |-  ( A. d e. Cat E! f f e. ( C Func d ) -> ( C e. _V /\ (/) = ( Base ` C ) ) )
32 12 31 impbii 
 |-  ( ( C e. _V /\ (/) = ( Base ` C ) ) <-> A. d e. Cat E! f f e. ( C Func d ) )