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

Metamath Proof Explorer

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