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

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 )