Metamath Proof Explorer


Theorem ssc1

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

Ref Expression
Hypotheses isssc.1
|- ( ph -> H Fn ( S X. S ) )
isssc.2
|- ( ph -> J Fn ( T X. T ) )
ssc1.3
|- ( ph -> H C_cat J )
Assertion ssc1
|- ( ph -> S C_ T )

Proof

Step Hyp Ref Expression
1 isssc.1
 |-  ( ph -> H Fn ( S X. S ) )
2 isssc.2
 |-  ( ph -> J Fn ( T X. T ) )
3 ssc1.3
 |-  ( ph -> H C_cat J )
4 sscrel
 |-  Rel C_cat
5 4 brrelex2i
 |-  ( H C_cat J -> J e. _V )
6 3 5 syl
 |-  ( ph -> J e. _V )
7 2 ssclem
 |-  ( ph -> ( J e. _V <-> T e. _V ) )
8 6 7 mpbid
 |-  ( ph -> T e. _V )
9 1 2 8 isssc
 |-  ( ph -> ( H C_cat J <-> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) )
10 3 9 mpbid
 |-  ( ph -> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) )
11 10 simpld
 |-  ( ph -> S C_ T )