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→∅⊆catHom𝑓⁡C

Proof

Step Hyp Ref Expression
1 0ss ⊢∅⊆BaseC
2 1 a1i ⊢C∈Cat→∅⊆BaseC
3 ral0 ⊢∀x∈∅∀y∈∅x∅y⊆xHom𝑓⁡Cy
4 3 a1i ⊢C∈Cat→∀x∈∅∀y∈∅x∅y⊆xHom𝑓⁡Cy
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 ⊢BaseC=BaseC
14 12 13 homffn ⊢Hom𝑓⁡CFnBaseC×BaseC
15 14 a1i ⊢C∈Cat→Hom𝑓⁡CFnBaseC×BaseC
16 fvexd ⊢C∈Cat→BaseC∈V
17 11 15 16 isssc ⊢C∈Cat→∅⊆catHom𝑓⁡C↔∅⊆BaseC∧∀x∈∅∀y∈∅x∅y⊆xHom𝑓⁡Cy
18 2 4 17 mpbir2and ⊢C∈Cat→∅⊆catHom𝑓⁡C