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