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