This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0subcat

Description: For any category C , the empty set is a (full) subcategory of C , see example 4.3(1.a) in Adamek p. 48. (Contributed by AV, 23-Apr-2020)

Ref Expression
Assertion 0subcat 
|- ( C e. Cat -> (/) e. ( Subcat ` C ) )

Proof

Step Hyp Ref Expression
1 0ssc 
 |-  ( C e. Cat -> (/) C_cat ( Homf ` C ) )
2 ral0 
 |-  A. x e. (/) ( ( ( Id ` C ) ` x ) e. ( x (/) x ) /\ A. y e. (/) A. z e. (/) A. f e. ( x (/) y ) A. g e. ( y (/) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x (/) z ) )
3 2 a1i 
 |-  ( C e. Cat -> A. x e. (/) ( ( ( Id ` C ) ` x ) e. ( x (/) x ) /\ A. y e. (/) A. z e. (/) A. f e. ( x (/) y ) A. g e. ( y (/) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x (/) z ) ) )
4 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
5 eqid 
 |-  ( Id ` C ) = ( Id ` C )
6 eqid 
 |-  ( comp ` C ) = ( comp ` C )
7 id 
 |-  ( C e. Cat -> C e. Cat )
8 f0 
 |-  (/) : (/) --> (/)
9 ffn 
 |-  ( (/) : (/) --> (/) -> (/) Fn (/) )
10 8 9 ax-mp 
 |-  (/) Fn (/)
11 0xp 
 |-  ( (/) X. (/) ) = (/)
12 11 fneq2i 
 |-  ( (/) Fn ( (/) X. (/) ) <-> (/) Fn (/) )
13 10 12 mpbir 
 |-  (/) Fn ( (/) X. (/) )
14 13 a1i 
 |-  ( C e. Cat -> (/) Fn ( (/) X. (/) ) )
15 4 5 6 7 14 issubc2 
 |-  ( C e. Cat -> ( (/) e. ( Subcat ` C ) <-> ( (/) C_cat ( Homf ` C ) /\ A. x e. (/) ( ( ( Id ` C ) ` x ) e. ( x (/) x ) /\ A. y e. (/) A. z e. (/) A. f e. ( x (/) y ) A. g e. ( y (/) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x (/) z ) ) ) ) )
16 1 3 15 mpbir2and 
 |-  ( C e. Cat -> (/) e. ( Subcat ` C ) )