This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) → ∅ = ( Base ‘ 𝐶 ) )
2 eqidd ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
3 eqidd ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) )
4 simpl ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) → 𝐶 ∈ 𝑉 )
5 noel ⊢ ¬ 𝑥 ∈ ∅
6 5 pm2.21i ⊢ ( 𝑥 ∈ ∅ → ∅ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
7 6 adantl ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ 𝑥 ∈ ∅ ) → ∅ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
8 simpr1 ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ) → 𝑥 ∈ ∅ )
9 5 pm2.21i ⊢ ( 𝑥 ∈ ∅ → ( ∅ ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 )
10 8 9 syl ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ) → ( ∅ ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 )
11 simpr1 ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑥 ∈ ∅ )
12 5 pm2.21i ⊢ ( 𝑥 ∈ ∅ → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ∅ ) = 𝑓 )
13 11 12 syl ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ∅ ) = 𝑓 )
14 simp21 ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑥 ∈ ∅ )
15 5 pm2.21i ⊢ ( 𝑥 ∈ ∅ → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
16 14 15 syl ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
17 simp2ll ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ) ∧ ( 𝑧 ∈ ∅ ∧ 𝑤 ∈ ∅ ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) → 𝑥 ∈ ∅ )
18 5 pm2.21i ⊢ ( 𝑥 ∈ ∅ → ( ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( ℎ ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) )
19 17 18 syl ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ) ∧ ( 𝑧 ∈ ∅ ∧ 𝑤 ∈ ∅ ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) → ( ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( ℎ ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) )
20 1 2 3 4 7 10 13 16 19 iscatd ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )