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 ∈ Cat → ∅ ∈ Subcat ⁡ C

Proof

Step Hyp Ref Expression
1 0ssc ⊢ C ∈ Cat → ∅ ⊆ cat Hom 𝑓 ⁡ C
2 ral0 ⊢ ∀ x ∈ ∅ Id ⁡ C ⁡ x ∈ x ∅ x ∧ ∀ y ∈ ∅ ∀ z ∈ ∅ ∀ f ∈ x ∅ y ∀ g ∈ y ∅ z g x y comp ⁡ C z f ∈ x ∅ z
3 2 a1i ⊢ C ∈ Cat → ∀ x ∈ ∅ Id ⁡ C ⁡ x ∈ x ∅ x ∧ ∀ y ∈ ∅ ∀ z ∈ ∅ ∀ f ∈ x ∅ y ∀ g ∈ y ∅ z g x y comp ⁡ C z f ∈ x ∅ z
4 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
5 eqid ⊢ Id ⁡ C = Id ⁡ C
6 eqid ⊢ comp ⁡ C = comp ⁡ C
7 id ⊢ C ∈ Cat → C ∈ Cat
8 f0 ⊢ ∅ : ∅ ⟶ ∅
9 ffn ⊢ ∅ : ∅ ⟶ ∅ → ∅ Fn ∅
10 8 9 ax-mp ⊢ ∅ Fn ∅
11 0xp ⊢ ∅ × ∅ = ∅
12 11 fneq2i ⊢ ∅ Fn ∅ × ∅ ↔ ∅ Fn ∅
13 10 12 mpbir ⊢ ∅ Fn ∅ × ∅
14 13 a1i ⊢ C ∈ Cat → ∅ Fn ∅ × ∅
15 4 5 6 7 14 issubc2 ⊢ C ∈ Cat → ∅ ∈ Subcat ⁡ C ↔ ∅ ⊆ cat Hom 𝑓 ⁡ C ∧ ∀ x ∈ ∅ Id ⁡ C ⁡ x ∈ x ∅ x ∧ ∀ y ∈ ∅ ∀ z ∈ ∅ ∀ f ∈ x ∅ y ∀ g ∈ y ∅ z g x y comp ⁡ C z f ∈ x ∅ z
16 1 3 15 mpbir2and ⊢ C ∈ Cat → ∅ ∈ Subcat ⁡ C