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

Metamath Proof Explorer

Theorem subcss1

Description: The objects of a subcategory are a subset of the objects of the original. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subcss1.1 ⊢ φ → J ∈ Subcat ⁡ C
subcss1.2 ⊢ φ → J Fn S × S
subcss1.b ⊢ B = Base C
Assertion subcss1 ⊢ φ → S ⊆ B

Proof

Step Hyp Ref Expression
1 subcss1.1 ⊢ φ → J ∈ Subcat ⁡ C
2 subcss1.2 ⊢ φ → J Fn S × S
3 subcss1.b ⊢ B = Base C
4 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
5 4 3 homffn ⊢ Hom 𝑓 ⁡ C Fn B × B
6 5 a1i ⊢ φ → Hom 𝑓 ⁡ C Fn B × B
7 1 4 subcssc ⊢ φ → J ⊆ cat Hom 𝑓 ⁡ C
8 2 6 7 ssc1 ⊢ φ → S ⊆ B