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

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 ( 𝐶 ∈ Cat → ∅ ∈ ( Subcat ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 0ssc ⊢ ( 𝐶 ∈ Cat → ∅ ⊆cat ( Homf ‘ 𝐶 ) )
2 ral0 ⊢ ∀ 𝑥 ∈ ∅ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ∅ 𝑥 ) ∧ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑓 ∈ ( 𝑥 ∅ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ∅ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ∅ 𝑧 ) )
3 2 a1i ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ ∅ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ∅ 𝑥 ) ∧ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑓 ∈ ( 𝑥 ∅ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ∅ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ∅ 𝑧 ) ) )
4 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
5 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
6 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
7 id ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ 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 ⊢ ( 𝐶 ∈ Cat → ∅ Fn ( ∅ × ∅ ) )
15 4 5 6 7 14 issubc2 ⊢ ( 𝐶 ∈ Cat → ( ∅ ∈ ( Subcat ‘ 𝐶 ) ↔ ( ∅ ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ ∅ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ∅ 𝑥 ) ∧ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑓 ∈ ( 𝑥 ∅ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ∅ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ∅ 𝑧 ) ) ) ) )
16 1 3 15 mpbir2and ⊢ ( 𝐶 ∈ Cat → ∅ ∈ ( Subcat ‘ 𝐶 ) )