Metamath Proof Explorer

Theorem 0catg

Description: Any structure with an empty set of objects is a category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Assertion 0catg ⊢ C ∈ V ∧ ∅ = Base C → C ∈ Cat

Proof

Step Hyp Ref Expression
1 simpr ⊢ C ∈ V ∧ ∅ = Base C → ∅ = Base C
2 eqidd ⊢ C ∈ V ∧ ∅ = Base C → Hom ⁡ C = Hom ⁡ C
3 eqidd ⊢ C ∈ V ∧ ∅ = Base C → comp ⁡ C = comp ⁡ C
4 simpl ⊢ C ∈ V ∧ ∅ = Base C → C ∈ V
5 noel ⊢ ¬ x ∈ ∅
6 5 pm2.21i ⊢ x ∈ ∅ → ∅ ∈ x Hom ⁡ C x
7 6 adantl ⊢ C ∈ V ∧ ∅ = Base C ∧ x ∈ ∅ → ∅ ∈ x Hom ⁡ C x
8 simpr1 ⊢ C ∈ V ∧ ∅ = Base C ∧ x ∈ ∅ ∧ y ∈ ∅ ∧ f ∈ y Hom ⁡ C x → x ∈ ∅
9 5 pm2.21i ⊢ x ∈ ∅ → ∅ y x comp ⁡ C x f = f
10 8 9 syl ⊢ C ∈ V ∧ ∅ = Base C ∧ x ∈ ∅ ∧ y ∈ ∅ ∧ f ∈ y Hom ⁡ C x → ∅ y x comp ⁡ C x f = f
11 simpr1 ⊢ C ∈ V ∧ ∅ = Base C ∧ x ∈ ∅ ∧ y ∈ ∅ ∧ f ∈ x Hom ⁡ C y → x ∈ ∅
12 5 pm2.21i ⊢ x ∈ ∅ → f x x comp ⁡ C y ∅ = f
13 11 12 syl ⊢ C ∈ V ∧ ∅ = Base C ∧ x ∈ ∅ ∧ y ∈ ∅ ∧ f ∈ x Hom ⁡ C y → f x x comp ⁡ C y ∅ = f
14 simp21 ⊢ C ∈ V ∧ ∅ = Base C ∧ x ∈ ∅ ∧ y ∈ ∅ ∧ z ∈ ∅ ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → x ∈ ∅
15 5 pm2.21i ⊢ x ∈ ∅ → g x y comp ⁡ C z f ∈ x Hom ⁡ C z
16 14 15 syl ⊢ C ∈ V ∧ ∅ = Base C ∧ x ∈ ∅ ∧ y ∈ ∅ ∧ z ∈ ∅ ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z → g x y comp ⁡ C z f ∈ x Hom ⁡ C z
17 simp2ll ⊢ C ∈ V ∧ ∅ = Base C ∧ x ∈ ∅ ∧ y ∈ ∅ ∧ z ∈ ∅ ∧ w ∈ ∅ ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ h ∈ z Hom ⁡ C w → x ∈ ∅
18 5 pm2.21i ⊢ x ∈ ∅ → h y z comp ⁡ C w g x y comp ⁡ C w f = h x z comp ⁡ C w g x y comp ⁡ C z f
19 17 18 syl ⊢ C ∈ V ∧ ∅ = Base C ∧ x ∈ ∅ ∧ y ∈ ∅ ∧ z ∈ ∅ ∧ w ∈ ∅ ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ h ∈ z Hom ⁡ C w → h y z comp ⁡ C w g x y comp ⁡ C w f = h x z comp ⁡ C w g x y comp ⁡ C z f
20 1 2 3 4 7 10 13 16 19 iscatd ⊢ C ∈ V ∧ ∅ = Base C → C ∈ Cat