Metamath Proof Explorer

Theorem subthinc

Description: A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024)

Ref Expression
Hypotheses subthinc.1 
|- D = ( C |`cat J )
subthinc.j 
|- ( ph -> J e. ( Subcat ` C ) )
subthinc.c 
|- ( ph -> C e. ThinCat )
Assertion subthinc 
|- ( ph -> D e. ThinCat )

Proof

Step Hyp Ref Expression
1 subthinc.1 
 |-  D = ( C |`cat J )
2 subthinc.j 
 |-  ( ph -> J e. ( Subcat ` C ) )
3 subthinc.c 
 |-  ( ph -> C e. ThinCat )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 eqidd 
 |-  ( ph -> dom dom J = dom dom J )
6 2 5 subcfn 
 |-  ( ph -> J Fn ( dom dom J X. dom dom J ) )
7 2 6 4 subcss1 
 |-  ( ph -> dom dom J C_ ( Base ` C ) )
8 1 4 3 6 7 rescbas 
 |-  ( ph -> dom dom J = ( Base ` D ) )
9 1 4 3 6 7 reschom 
 |-  ( ph -> J = ( Hom ` D ) )
10 2 adantr 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> J e. ( Subcat ` C ) )
11 6 adantr 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> J Fn ( dom dom J X. dom dom J ) )
12 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
13 simprl 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> x e. dom dom J )
14 simprr 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> y e. dom dom J )
15 10 11 12 13 14 subcss2 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> ( x J y ) C_ ( x ( Hom ` C ) y ) )
16 3 adantr 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> C e. ThinCat )
17 7 adantr 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> dom dom J C_ ( Base ` C ) )
18 17 13 sseldd 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> x e. ( Base ` C ) )
19 17 14 sseldd 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> y e. ( Base ` C ) )
20 16 18 19 4 12 thincmo 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> E* f f e. ( x ( Hom ` C ) y ) )
21 mosssn2 
 |-  ( E* f f e. ( x ( Hom ` C ) y ) <-> E. f ( x ( Hom ` C ) y ) C_ { f } )
22 20 21 sylib 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> E. f ( x ( Hom ` C ) y ) C_ { f } )
23 sstr2 
 |-  ( ( x J y ) C_ ( x ( Hom ` C ) y ) -> ( ( x ( Hom ` C ) y ) C_ { f } -> ( x J y ) C_ { f } ) )
24 23 eximdv 
 |-  ( ( x J y ) C_ ( x ( Hom ` C ) y ) -> ( E. f ( x ( Hom ` C ) y ) C_ { f } -> E. f ( x J y ) C_ { f } ) )
25 15 22 24 sylc 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> E. f ( x J y ) C_ { f } )
26 mosssn2 
 |-  ( E* f f e. ( x J y ) <-> E. f ( x J y ) C_ { f } )
27 25 26 sylibr 
 |-  ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> E* f f e. ( x J y ) )
28 1 2 subccat 
 |-  ( ph -> D e. Cat )
29 8 9 27 28 isthincd 
 |-  ( ph -> D e. ThinCat )