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→∅⊆catHom𝑓⁡C
2 ral0 ⊢∀x∈∅Id⁡C⁡x∈x∅x∧∀y∈∅∀z∈∅∀f∈x∅y∀g∈y∅zgxycomp⁡Czf∈x∅z
3 2 a1i ⊢C∈Cat→∀x∈∅Id⁡C⁡x∈x∅x∧∀y∈∅∀z∈∅∀f∈x∅y∀g∈y∅zgxycomp⁡Czf∈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↔∅⊆catHom𝑓⁡C∧∀x∈∅Id⁡C⁡x∈x∅x∧∀y∈∅∀z∈∅∀f∈x∅y∀g∈y∅zgxycomp⁡Czf∈x∅z
16 1 3 15 mpbir2and ⊢C∈Cat→∅∈Subcat⁡C