# Metamath Proof Explorer

## Theorem subsubc

Description: A subcategory of a subcategory is a subcategory. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypothesis subsubc.d ${⊢}{D}={C}{↾}_{\mathrm{cat}}{H}$
Assertion subsubc ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \left({J}\in \mathrm{Subcat}\left({D}\right)↔\left({J}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\right)$

### Proof

Step Hyp Ref Expression
1 subsubc.d ${⊢}{D}={C}{↾}_{\mathrm{cat}}{H}$
2 id ${⊢}{J}\in \mathrm{Subcat}\left({D}\right)\to {J}\in \mathrm{Subcat}\left({D}\right)$
3 eqid ${⊢}{\mathrm{Hom}}_{𝑓}\left({D}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
4 2 3 subcssc ${⊢}{J}\in \mathrm{Subcat}\left({D}\right)\to {J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({D}\right)$
5 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
6 subcrcl ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to {C}\in \mathrm{Cat}$
7 id ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to {H}\in \mathrm{Subcat}\left({C}\right)$
8 eqidd ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \mathrm{dom}\mathrm{dom}{H}=\mathrm{dom}\mathrm{dom}{H}$
9 7 8 subcfn ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to {H}Fn\left(\mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}\right)$
10 7 9 5 subcss1 ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \mathrm{dom}\mathrm{dom}{H}\subseteq {\mathrm{Base}}_{{C}}$
11 1 5 6 9 10 reschomf ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to {H}={\mathrm{Hom}}_{𝑓}\left({D}\right)$
12 11 breq2d ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \left({J}{\subseteq }_{\mathrm{cat}}{H}↔{J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({D}\right)\right)$
13 4 12 syl5ibr ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \left({J}\in \mathrm{Subcat}\left({D}\right)\to {J}{\subseteq }_{\mathrm{cat}}{H}\right)$
14 13 pm4.71rd ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \left({J}\in \mathrm{Subcat}\left({D}\right)↔\left({J}{\subseteq }_{\mathrm{cat}}{H}\wedge {J}\in \mathrm{Subcat}\left({D}\right)\right)\right)$
15 simpr ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to {J}{\subseteq }_{\mathrm{cat}}{H}$
16 simpl ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to {H}\in \mathrm{Subcat}\left({C}\right)$
17 eqid ${⊢}{\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({C}\right)$
18 16 17 subcssc ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to {H}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({C}\right)$
19 ssctr ${⊢}\left({J}{\subseteq }_{\mathrm{cat}}{H}\wedge {H}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({C}\right)\right)\to {J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({C}\right)$
20 15 18 19 syl2anc ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to {J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({C}\right)$
21 12 biimpa ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to {J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({D}\right)$
22 20 21 2thd ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \left({J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({C}\right)↔{J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({D}\right)\right)$
23 16 adantr ${⊢}\left(\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\wedge {x}\in \mathrm{dom}\mathrm{dom}{J}\right)\to {H}\in \mathrm{Subcat}\left({C}\right)$
24 9 adantr ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to {H}Fn\left(\mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}\right)$
25 24 adantr ${⊢}\left(\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\wedge {x}\in \mathrm{dom}\mathrm{dom}{J}\right)\to {H}Fn\left(\mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}\right)$
26 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
27 eqidd ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \mathrm{dom}\mathrm{dom}{J}=\mathrm{dom}\mathrm{dom}{J}$
28 15 27 sscfn1 ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to {J}Fn\left(\mathrm{dom}\mathrm{dom}{J}×\mathrm{dom}\mathrm{dom}{J}\right)$
29 28 24 15 ssc1 ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \mathrm{dom}\mathrm{dom}{J}\subseteq \mathrm{dom}\mathrm{dom}{H}$
30 29 sselda ${⊢}\left(\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\wedge {x}\in \mathrm{dom}\mathrm{dom}{J}\right)\to {x}\in \mathrm{dom}\mathrm{dom}{H}$
31 1 23 25 26 30 subcid ${⊢}\left(\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\wedge {x}\in \mathrm{dom}\mathrm{dom}{J}\right)\to \mathrm{Id}\left({C}\right)\left({x}\right)=\mathrm{Id}\left({D}\right)\left({x}\right)$
32 31 eleq1d ${⊢}\left(\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\wedge {x}\in \mathrm{dom}\mathrm{dom}{J}\right)\to \left(\mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{J}{x}\right)↔\mathrm{Id}\left({D}\right)\left({x}\right)\in \left({x}{J}{x}\right)\right)$
33 32 ralbidva ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \left(\forall {x}\in \mathrm{dom}\mathrm{dom}{J}\phantom{\rule{.4em}{0ex}}\mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{J}{x}\right)↔\forall {x}\in \mathrm{dom}\mathrm{dom}{J}\phantom{\rule{.4em}{0ex}}\mathrm{Id}\left({D}\right)\left({x}\right)\in \left({x}{J}{x}\right)\right)$
34 1 oveq1i ${⊢}{D}{↾}_{\mathrm{cat}}{J}=\left({C}{↾}_{\mathrm{cat}}{H}\right){↾}_{\mathrm{cat}}{J}$
35 6 adantr ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to {C}\in \mathrm{Cat}$
36 dmexg ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \mathrm{dom}{H}\in \mathrm{V}$
37 36 dmexd ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \mathrm{dom}\mathrm{dom}{H}\in \mathrm{V}$
38 37 adantr ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \mathrm{dom}\mathrm{dom}{H}\in \mathrm{V}$
39 35 24 28 38 29 rescabs ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \left({C}{↾}_{\mathrm{cat}}{H}\right){↾}_{\mathrm{cat}}{J}={C}{↾}_{\mathrm{cat}}{J}$
40 34 39 syl5req ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to {C}{↾}_{\mathrm{cat}}{J}={D}{↾}_{\mathrm{cat}}{J}$
41 40 eleq1d ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \left({C}{↾}_{\mathrm{cat}}{J}\in \mathrm{Cat}↔{D}{↾}_{\mathrm{cat}}{J}\in \mathrm{Cat}\right)$
42 22 33 41 3anbi123d ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \left(\left({J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({C}\right)\wedge \forall {x}\in \mathrm{dom}\mathrm{dom}{J}\phantom{\rule{.4em}{0ex}}\mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{J}{x}\right)\wedge {C}{↾}_{\mathrm{cat}}{J}\in \mathrm{Cat}\right)↔\left({J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({D}\right)\wedge \forall {x}\in \mathrm{dom}\mathrm{dom}{J}\phantom{\rule{.4em}{0ex}}\mathrm{Id}\left({D}\right)\left({x}\right)\in \left({x}{J}{x}\right)\wedge {D}{↾}_{\mathrm{cat}}{J}\in \mathrm{Cat}\right)\right)$
43 eqid ${⊢}{C}{↾}_{\mathrm{cat}}{J}={C}{↾}_{\mathrm{cat}}{J}$
44 17 26 43 35 28 issubc3 ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \left({J}\in \mathrm{Subcat}\left({C}\right)↔\left({J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({C}\right)\wedge \forall {x}\in \mathrm{dom}\mathrm{dom}{J}\phantom{\rule{.4em}{0ex}}\mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{J}{x}\right)\wedge {C}{↾}_{\mathrm{cat}}{J}\in \mathrm{Cat}\right)\right)$
45 eqid ${⊢}\mathrm{Id}\left({D}\right)=\mathrm{Id}\left({D}\right)$
46 eqid ${⊢}{D}{↾}_{\mathrm{cat}}{J}={D}{↾}_{\mathrm{cat}}{J}$
47 1 7 subccat ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to {D}\in \mathrm{Cat}$
48 47 adantr ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to {D}\in \mathrm{Cat}$
49 3 45 46 48 28 issubc3 ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \left({J}\in \mathrm{Subcat}\left({D}\right)↔\left({J}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({D}\right)\wedge \forall {x}\in \mathrm{dom}\mathrm{dom}{J}\phantom{\rule{.4em}{0ex}}\mathrm{Id}\left({D}\right)\left({x}\right)\in \left({x}{J}{x}\right)\wedge {D}{↾}_{\mathrm{cat}}{J}\in \mathrm{Cat}\right)\right)$
50 42 44 49 3bitr4rd ${⊢}\left({H}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\to \left({J}\in \mathrm{Subcat}\left({D}\right)↔{J}\in \mathrm{Subcat}\left({C}\right)\right)$
51 50 pm5.32da ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \left(\left({J}{\subseteq }_{\mathrm{cat}}{H}\wedge {J}\in \mathrm{Subcat}\left({D}\right)\right)↔\left({J}{\subseteq }_{\mathrm{cat}}{H}\wedge {J}\in \mathrm{Subcat}\left({C}\right)\right)\right)$
52 14 51 bitrd ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \left({J}\in \mathrm{Subcat}\left({D}\right)↔\left({J}{\subseteq }_{\mathrm{cat}}{H}\wedge {J}\in \mathrm{Subcat}\left({C}\right)\right)\right)$
53 52 biancomd ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \left({J}\in \mathrm{Subcat}\left({D}\right)↔\left({J}\in \mathrm{Subcat}\left({C}\right)\wedge {J}{\subseteq }_{\mathrm{cat}}{H}\right)\right)$