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=CcatJ
subthinc.j φJSubcatC
subthinc.c No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
Assertion subthinc Could not format assertion : No typesetting found for |- ( ph -> D e. ThinCat ) with typecode |-

Proof

Step Hyp Ref Expression
1 subthinc.1 D=CcatJ
2 subthinc.j φJSubcatC
3 subthinc.c Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
4 eqid BaseC=BaseC
5 eqidd φdomdomJ=domdomJ
6 2 5 subcfn φJFndomdomJ×domdomJ
7 2 6 4 subcss1 φdomdomJBaseC
8 1 4 3 6 7 rescbas φdomdomJ=BaseD
9 1 4 3 6 7 reschom φJ=HomD
10 2 adantr φxdomdomJydomdomJJSubcatC
11 6 adantr φxdomdomJydomdomJJFndomdomJ×domdomJ
12 eqid HomC=HomC
13 simprl φxdomdomJydomdomJxdomdomJ
14 simprr φxdomdomJydomdomJydomdomJ
15 10 11 12 13 14 subcss2 φxdomdomJydomdomJxJyxHomCy
16 3 adantr Could not format ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> C e. ThinCat ) : No typesetting found for |- ( ( ph /\ ( x e. dom dom J /\ y e. dom dom J ) ) -> C e. ThinCat ) with typecode |-
17 7 adantr φxdomdomJydomdomJdomdomJBaseC
18 17 13 sseldd φxdomdomJydomdomJxBaseC
19 17 14 sseldd φxdomdomJydomdomJyBaseC
20 16 18 19 4 12 thincmo φxdomdomJydomdomJ*ffxHomCy
21 mosssn2 *ffxHomCyfxHomCyf
22 20 21 sylib φxdomdomJydomdomJfxHomCyf
23 sstr2 xJyxHomCyxHomCyfxJyf
24 23 eximdv xJyxHomCyfxHomCyffxJyf
25 15 22 24 sylc φxdomdomJydomdomJfxJyf
26 mosssn2 *ffxJyfxJyf
27 25 26 sylibr φxdomdomJydomdomJ*ffxJy
28 1 2 subccat φDCat
29 8 9 27 28 isthincd Could not format ( ph -> D e. ThinCat ) : No typesetting found for |- ( ph -> D e. ThinCat ) with typecode |-