Description: A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subthinc.1 | |
|
subthinc.j | |
||
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 |- |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subthinc.1 | |
|
2 | subthinc.j | |
|
3 | subthinc.c | Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |- | |
4 | eqid | |
|
5 | eqidd | |
|
6 | 2 5 | subcfn | |
7 | 2 6 4 | subcss1 | |
8 | 1 4 3 6 7 | rescbas | |
9 | 1 4 3 6 7 | reschom | |
10 | 2 | adantr | |
11 | 6 | adantr | |
12 | eqid | |
|
13 | simprl | |
|
14 | simprr | |
|
15 | 10 11 12 13 14 | subcss2 | |
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 | |
18 | 17 13 | sseldd | |
19 | 17 14 | sseldd | |
20 | 16 18 19 4 12 | thincmo | |
21 | mosssn2 | |
|
22 | 20 21 | sylib | |
23 | sstr2 | |
|
24 | 23 | eximdv | |
25 | 15 22 24 | sylc | |
26 | mosssn2 | |
|
27 | 25 26 | sylibr | |
28 | 1 2 | subccat | |
29 | 8 9 27 28 | isthincd | Could not format ( ph -> D e. ThinCat ) : No typesetting found for |- ( ph -> D e. ThinCat ) with typecode |- |