Theorem 0ssc

Description: For any category C , the empty set is a subcategory subset of C . (Contributed by AV, 23-Apr-2020)

	Ref	Expression
Assertion	0ssc	⊢ ( 𝐶 ∈ Cat → ∅ ⊆cat ( Homf ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ ( Base ‘ 𝐶 )
2	1	a1i	⊢ ( 𝐶 ∈ Cat → ∅ ⊆ ( Base ‘ 𝐶 ) )
3		ral0	⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 ∅ 𝑦 ) ⊆ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 )
4	3	a1i	⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 ∅ 𝑦 ) ⊆ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) )
5		f0	⊢ ∅ : ∅ ⟶ ∅
6		ffn	⊢ ( ∅ : ∅ ⟶ ∅ → ∅ Fn ∅ )
7	5 6	ax-mp	⊢ ∅ Fn ∅
8		xp0	⊢ ( ∅ × ∅ ) = ∅
9	8	fneq2i	⊢ ( ∅ Fn ( ∅ × ∅ ) ↔ ∅ Fn ∅ )
10	7 9	mpbir	⊢ ∅ Fn ( ∅ × ∅ )
11	10	a1i	⊢ ( 𝐶 ∈ Cat → ∅ Fn ( ∅ × ∅ ) )
12		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
13		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
14	12 13	homffn	⊢ ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
15	14	a1i	⊢ ( 𝐶 ∈ Cat → ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
16		fvexd	⊢ ( 𝐶 ∈ Cat → ( Base ‘ 𝐶 ) ∈ V )
17	11 15 16	isssc	⊢ ( 𝐶 ∈ Cat → ( ∅ ⊆cat ( Homf ‘ 𝐶 ) ↔ ( ∅ ⊆ ( Base ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 ∅ 𝑦 ) ⊆ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ) ) )
18	2 4 17	mpbir2and	⊢ ( 𝐶 ∈ Cat → ∅ ⊆cat ( Homf ‘ 𝐶 ) )