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 Cat cat Hom 𝑓 C

Proof

Step Hyp Ref Expression
1 0ss Base C
2 1 a1i C Cat Base C
3 ral0 x y x y x Hom 𝑓 C y
4 3 a1i C Cat x y x y x Hom 𝑓 C y
5 f0 :
6 ffn : Fn
7 5 6 ax-mp Fn
8 xp0 × =
9 8 fneq2i Fn × Fn
10 7 9 mpbir Fn ×
11 10 a1i C Cat Fn ×
12 eqid Hom 𝑓 C = Hom 𝑓 C
13 eqid Base C = Base C
14 12 13 homffn Hom 𝑓 C Fn Base C × Base C
15 14 a1i C Cat Hom 𝑓 C Fn Base C × Base C
16 fvexd C Cat Base C V
17 11 15 16 isssc C Cat cat Hom 𝑓 C Base C x y x y x Hom 𝑓 C y
18 2 4 17 mpbir2and C Cat cat Hom 𝑓 C