Metamath Proof Explorer


Theorem ssc2

Description: Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses ssc2.1 φ H Fn S × S
ssc2.2 φ H cat J
ssc2.3 φ X S
ssc2.4 φ Y S
Assertion ssc2 φ X H Y X J Y

Proof

Step Hyp Ref Expression
1 ssc2.1 φ H Fn S × S
2 ssc2.2 φ H cat J
3 ssc2.3 φ X S
4 ssc2.4 φ Y S
5 eqidd φ dom dom J = dom dom J
6 2 5 sscfn2 φ J Fn dom dom J × dom dom J
7 sscrel Rel cat
8 7 brrelex2i H cat J J V
9 dmexg J V dom J V
10 dmexg dom J V dom dom J V
11 2 8 9 10 4syl φ dom dom J V
12 1 6 11 isssc φ H cat J S dom dom J x S y S x H y x J y
13 2 12 mpbid φ S dom dom J x S y S x H y x J y
14 13 simprd φ x S y S x H y x J y
15 oveq1 x = X x H y = X H y
16 oveq1 x = X x J y = X J y
17 15 16 sseq12d x = X x H y x J y X H y X J y
18 oveq2 y = Y X H y = X H Y
19 oveq2 y = Y X J y = X J Y
20 18 19 sseq12d y = Y X H y X J y X H Y X J Y
21 17 20 rspc2va X S Y S x S y S x H y x J y X H Y X J Y
22 3 4 14 21 syl21anc φ X H Y X J Y