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

Metamath Proof Explorer

Theorem subcss2

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

Ref Expression
Hypotheses subcss1.1 ⊢ φ → J ∈ Subcat ⁡ C
subcss1.2 ⊢ φ → J Fn S × S
subcss2.h ⊢ H = Hom ⁡ C
subcss2.x ⊢ φ → X ∈ S
subcss2.y ⊢ φ → Y ∈ S
Assertion subcss2 ⊢ φ → X J Y ⊆ X H Y

Proof

Step Hyp Ref Expression
1 subcss1.1 ⊢ φ → J ∈ Subcat ⁡ C
2 subcss1.2 ⊢ φ → J Fn S × S
3 subcss2.h ⊢ H = Hom ⁡ C
4 subcss2.x ⊢ φ → X ∈ S
5 subcss2.y ⊢ φ → Y ∈ S
6 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
7 1 6 subcssc ⊢ φ → J ⊆ cat Hom 𝑓 ⁡ C
8 2 7 4 5 ssc2 ⊢ φ → X J Y ⊆ X Hom 𝑓 ⁡ C Y
9 eqid ⊢ Base C = Base C
10 1 2 9 subcss1 ⊢ φ → S ⊆ Base C
11 10 4 sseldd ⊢ φ → X ∈ Base C
12 10 5 sseldd ⊢ φ → Y ∈ Base C
13 6 9 3 11 12 homfval ⊢ φ → X Hom 𝑓 ⁡ C Y = X H Y
14 8 13 sseqtrd ⊢ φ → X J Y ⊆ X H Y