Metamath Proof Explorer

Theorem 0ssc

Description: For any category C , the empty set is a subcategory subset of C . (Contributed by AV, 23-Apr-2020)

Ref Expression
Assertion 0ssc 
|- ( C e. Cat -> (/) C_cat ( Homf ` C ) )

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ ( Base ` C )
2 1 a1i 
 |-  ( C e. Cat -> (/) C_ ( Base ` C ) )
3 ral0 
 |-  A. x e. (/) A. y e. (/) ( x (/) y ) C_ ( x ( Homf ` C ) y )
4 3 a1i 
 |-  ( C e. Cat -> A. x e. (/) A. y e. (/) ( x (/) y ) C_ ( x ( Homf ` C ) y ) )
5 f0 
 |-  (/) : (/) --> (/)
6 ffn 
 |-  ( (/) : (/) --> (/) -> (/) Fn (/) )
7 5 6 ax-mp 
 |-  (/) Fn (/)
8 xp0 
 |-  ( (/) X. (/) ) = (/)
9 8 fneq2i 
 |-  ( (/) Fn ( (/) X. (/) ) <-> (/) Fn (/) )
10 7 9 mpbir 
 |-  (/) Fn ( (/) X. (/) )
11 10 a1i 
 |-  ( C e. Cat -> (/) Fn ( (/) X. (/) ) )
12 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
13 eqid 
 |-  ( Base ` C ) = ( Base ` C )
14 12 13 homffn 
 |-  ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) )
15 14 a1i 
 |-  ( C e. Cat -> ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
16 fvexd 
 |-  ( C e. Cat -> ( Base ` C ) e. _V )
17 11 15 16 isssc 
 |-  ( C e. Cat -> ( (/) C_cat ( Homf ` C ) <-> ( (/) C_ ( Base ` C ) /\ A. x e. (/) A. y e. (/) ( x (/) y ) C_ ( x ( Homf ` C ) y ) ) ) )
18 2 4 17 mpbir2and 
 |-  ( C e. Cat -> (/) C_cat ( Homf ` C ) )