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 |`cat H )
Assertion subsubc 
|- ( H e. ( Subcat ` C ) -> ( J e. ( Subcat ` D ) <-> ( J e. ( Subcat ` C ) /\ J C_cat H ) ) )

Proof

Step Hyp Ref Expression
1 subsubc.d 
 |-  D = ( C |`cat H )
2 id 
 |-  ( J e. ( Subcat ` D ) -> J e. ( Subcat ` D ) )
3 eqid 
 |-  ( Homf ` D ) = ( Homf ` D )
4 2 3 subcssc 
 |-  ( J e. ( Subcat ` D ) -> J C_cat ( Homf ` D ) )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 subcrcl 
 |-  ( H e. ( Subcat ` C ) -> C e. Cat )
7 id 
 |-  ( H e. ( Subcat ` C ) -> H e. ( Subcat ` C ) )
8 eqidd 
 |-  ( H e. ( Subcat ` C ) -> dom dom H = dom dom H )
9 7 8 subcfn 
 |-  ( H e. ( Subcat ` C ) -> H Fn ( dom dom H X. dom dom H ) )
10 7 9 5 subcss1 
 |-  ( H e. ( Subcat ` C ) -> dom dom H C_ ( Base ` C ) )
11 1 5 6 9 10 reschomf 
 |-  ( H e. ( Subcat ` C ) -> H = ( Homf ` D ) )
12 11 breq2d 
 |-  ( H e. ( Subcat ` C ) -> ( J C_cat H <-> J C_cat ( Homf ` D ) ) )
13 4 12 imbitrrid 
 |-  ( H e. ( Subcat ` C ) -> ( J e. ( Subcat ` D ) -> J C_cat H ) )
14 13 pm4.71rd 
 |-  ( H e. ( Subcat ` C ) -> ( J e. ( Subcat ` D ) <-> ( J C_cat H /\ J e. ( Subcat ` D ) ) ) )
15 simpr 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> J C_cat H )
16 simpl 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> H e. ( Subcat ` C ) )
17 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
18 16 17 subcssc 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> H C_cat ( Homf ` C ) )
19 ssctr 
 |-  ( ( J C_cat H /\ H C_cat ( Homf ` C ) ) -> J C_cat ( Homf ` C ) )
20 15 18 19 syl2anc 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> J C_cat ( Homf ` C ) )
21 12 biimpa 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> J C_cat ( Homf ` D ) )
22 20 21 2thd 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> ( J C_cat ( Homf ` C ) <-> J C_cat ( Homf ` D ) ) )
23 16 adantr 
 |-  ( ( ( H e. ( Subcat ` C ) /\ J C_cat H ) /\ x e. dom dom J ) -> H e. ( Subcat ` C ) )
24 9 adantr 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> H Fn ( dom dom H X. dom dom H ) )
25 24 adantr 
 |-  ( ( ( H e. ( Subcat ` C ) /\ J C_cat H ) /\ x e. dom dom J ) -> H Fn ( dom dom H X. dom dom H ) )
26 eqid 
 |-  ( Id ` C ) = ( Id ` C )
27 eqidd 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> dom dom J = dom dom J )
28 15 27 sscfn1 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> J Fn ( dom dom J X. dom dom J ) )
29 28 24 15 ssc1 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> dom dom J C_ dom dom H )
30 29 sselda 
 |-  ( ( ( H e. ( Subcat ` C ) /\ J C_cat H ) /\ x e. dom dom J ) -> x e. dom dom H )
31 1 23 25 26 30 subcid 
 |-  ( ( ( H e. ( Subcat ` C ) /\ J C_cat H ) /\ x e. dom dom J ) -> ( ( Id ` C ) ` x ) = ( ( Id ` D ) ` x ) )
32 31 eleq1d 
 |-  ( ( ( H e. ( Subcat ` C ) /\ J C_cat H ) /\ x e. dom dom J ) -> ( ( ( Id ` C ) ` x ) e. ( x J x ) <-> ( ( Id ` D ) ` x ) e. ( x J x ) ) )
33 32 ralbidva 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> ( A. x e. dom dom J ( ( Id ` C ) ` x ) e. ( x J x ) <-> A. x e. dom dom J ( ( Id ` D ) ` x ) e. ( x J x ) ) )
34 1 oveq1i 
 |-  ( D |`cat J ) = ( ( C |`cat H ) |`cat J )
35 6 adantr 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> C e. Cat )
36 dmexg 
 |-  ( H e. ( Subcat ` C ) -> dom H e. _V )
37 36 dmexd 
 |-  ( H e. ( Subcat ` C ) -> dom dom H e. _V )
38 37 adantr 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> dom dom H e. _V )
39 35 24 28 38 29 rescabs 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) )
40 34 39 eqtr2id 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> ( C |`cat J ) = ( D |`cat J ) )
41 40 eleq1d 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> ( ( C |`cat J ) e. Cat <-> ( D |`cat J ) e. Cat ) )
42 22 33 41 3anbi123d 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> ( ( J C_cat ( Homf ` C ) /\ A. x e. dom dom J ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) <-> ( J C_cat ( Homf ` D ) /\ A. x e. dom dom J ( ( Id ` D ) ` x ) e. ( x J x ) /\ ( D |`cat J ) e. Cat ) ) )
43 eqid 
 |-  ( C |`cat J ) = ( C |`cat J )
44 17 26 43 35 28 issubc3 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> ( J e. ( Subcat ` C ) <-> ( J C_cat ( Homf ` C ) /\ A. x e. dom dom J ( ( Id ` C ) ` x ) e. ( x J x ) /\ ( C |`cat J ) e. Cat ) ) )
45 eqid 
 |-  ( Id ` D ) = ( Id ` D )
46 eqid 
 |-  ( D |`cat J ) = ( D |`cat J )
47 1 7 subccat 
 |-  ( H e. ( Subcat ` C ) -> D e. Cat )
48 47 adantr 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> D e. Cat )
49 3 45 46 48 28 issubc3 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> ( J e. ( Subcat ` D ) <-> ( J C_cat ( Homf ` D ) /\ A. x e. dom dom J ( ( Id ` D ) ` x ) e. ( x J x ) /\ ( D |`cat J ) e. Cat ) ) )
50 42 44 49 3bitr4rd 
 |-  ( ( H e. ( Subcat ` C ) /\ J C_cat H ) -> ( J e. ( Subcat ` D ) <-> J e. ( Subcat ` C ) ) )
51 50 pm5.32da 
 |-  ( H e. ( Subcat ` C ) -> ( ( J C_cat H /\ J e. ( Subcat ` D ) ) <-> ( J C_cat H /\ J e. ( Subcat ` C ) ) ) )
52 14 51 bitrd 
 |-  ( H e. ( Subcat ` C ) -> ( J e. ( Subcat ` D ) <-> ( J C_cat H /\ J e. ( Subcat ` C ) ) ) )
53 52 biancomd 
 |-  ( H e. ( Subcat ` C ) -> ( J e. ( Subcat ` D ) <-> ( J e. ( Subcat ` C ) /\ J C_cat H ) ) )