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 ‘ 𝐶 ) )