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 𝐷 = ( 𝐶cat 𝐻 )
Assertion subsubc ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → ( 𝐽 ∈ ( Subcat ‘ 𝐷 ) ↔ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 subsubc.d 𝐷 = ( 𝐶cat 𝐻 )
2 id ( 𝐽 ∈ ( Subcat ‘ 𝐷 ) → 𝐽 ∈ ( Subcat ‘ 𝐷 ) )
3 eqid ( Homf𝐷 ) = ( Homf𝐷 )
4 2 3 subcssc ( 𝐽 ∈ ( Subcat ‘ 𝐷 ) → 𝐽cat ( Homf𝐷 ) )
5 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 subcrcl ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat )
7 id ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )
8 eqidd ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → dom dom 𝐻 = dom dom 𝐻 )
9 7 8 subcfn ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → 𝐻 Fn ( dom dom 𝐻 × dom dom 𝐻 ) )
10 7 9 5 subcss1 ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → dom dom 𝐻 ⊆ ( Base ‘ 𝐶 ) )
11 1 5 6 9 10 reschomf ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → 𝐻 = ( Homf𝐷 ) )
12 11 breq2d ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → ( 𝐽cat 𝐻𝐽cat ( Homf𝐷 ) ) )
13 4 12 syl5ibr ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → ( 𝐽 ∈ ( Subcat ‘ 𝐷 ) → 𝐽cat 𝐻 ) )
14 13 pm4.71rd ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → ( 𝐽 ∈ ( Subcat ‘ 𝐷 ) ↔ ( 𝐽cat 𝐻𝐽 ∈ ( Subcat ‘ 𝐷 ) ) ) )
15 simpr ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → 𝐽cat 𝐻 )
16 simpl ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )
17 eqid ( Homf𝐶 ) = ( Homf𝐶 )
18 16 17 subcssc ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → 𝐻cat ( Homf𝐶 ) )
19 ssctr ( ( 𝐽cat 𝐻𝐻cat ( Homf𝐶 ) ) → 𝐽cat ( Homf𝐶 ) )
20 15 18 19 syl2anc ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → 𝐽cat ( Homf𝐶 ) )
21 12 biimpa ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → 𝐽cat ( Homf𝐷 ) )
22 20 21 2thd ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → ( 𝐽cat ( Homf𝐶 ) ↔ 𝐽cat ( Homf𝐷 ) ) )
23 16 adantr ( ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) ∧ 𝑥 ∈ dom dom 𝐽 ) → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )
24 9 adantr ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → 𝐻 Fn ( dom dom 𝐻 × dom dom 𝐻 ) )
25 24 adantr ( ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) ∧ 𝑥 ∈ dom dom 𝐽 ) → 𝐻 Fn ( dom dom 𝐻 × dom dom 𝐻 ) )
26 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
27 eqidd ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → dom dom 𝐽 = dom dom 𝐽 )
28 15 27 sscfn1 ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → 𝐽 Fn ( dom dom 𝐽 × dom dom 𝐽 ) )
29 28 24 15 ssc1 ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → dom dom 𝐽 ⊆ dom dom 𝐻 )
30 29 sselda ( ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) ∧ 𝑥 ∈ dom dom 𝐽 ) → 𝑥 ∈ dom dom 𝐻 )
31 1 23 25 26 30 subcid ( ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) ∧ 𝑥 ∈ dom dom 𝐽 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) )
32 31 eleq1d ( ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) ∧ 𝑥 ∈ dom dom 𝐽 ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
33 32 ralbidva ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → ( ∀ 𝑥 ∈ dom dom 𝐽 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ∀ 𝑥 ∈ dom dom 𝐽 ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
34 1 oveq1i ( 𝐷cat 𝐽 ) = ( ( 𝐶cat 𝐻 ) ↾cat 𝐽 )
35 6 adantr ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → 𝐶 ∈ Cat )
36 dmexg ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → dom 𝐻 ∈ V )
37 36 dmexd ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → dom dom 𝐻 ∈ V )
38 37 adantr ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → dom dom 𝐻 ∈ V )
39 35 24 28 38 29 rescabs ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → ( ( 𝐶cat 𝐻 ) ↾cat 𝐽 ) = ( 𝐶cat 𝐽 ) )
40 34 39 eqtr2id ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → ( 𝐶cat 𝐽 ) = ( 𝐷cat 𝐽 ) )
41 40 eleq1d ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → ( ( 𝐶cat 𝐽 ) ∈ Cat ↔ ( 𝐷cat 𝐽 ) ∈ Cat ) )
42 22 33 41 3anbi123d ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → ( ( 𝐽cat ( Homf𝐶 ) ∧ ∀ 𝑥 ∈ dom dom 𝐽 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶cat 𝐽 ) ∈ Cat ) ↔ ( 𝐽cat ( Homf𝐷 ) ∧ ∀ 𝑥 ∈ dom dom 𝐽 ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐷cat 𝐽 ) ∈ Cat ) ) )
43 eqid ( 𝐶cat 𝐽 ) = ( 𝐶cat 𝐽 )
44 17 26 43 35 28 issubc3 ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽cat ( Homf𝐶 ) ∧ ∀ 𝑥 ∈ dom dom 𝐽 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐶cat 𝐽 ) ∈ Cat ) ) )
45 eqid ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
46 eqid ( 𝐷cat 𝐽 ) = ( 𝐷cat 𝐽 )
47 1 7 subccat ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → 𝐷 ∈ Cat )
48 47 adantr ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → 𝐷 ∈ Cat )
49 3 45 46 48 28 issubc3 ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → ( 𝐽 ∈ ( Subcat ‘ 𝐷 ) ↔ ( 𝐽cat ( Homf𝐷 ) ∧ ∀ 𝑥 ∈ dom dom 𝐽 ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ( 𝐷cat 𝐽 ) ∈ Cat ) ) )
50 42 44 49 3bitr4rd ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) → ( 𝐽 ∈ ( Subcat ‘ 𝐷 ) ↔ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) )
51 50 pm5.32da ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → ( ( 𝐽cat 𝐻𝐽 ∈ ( Subcat ‘ 𝐷 ) ) ↔ ( 𝐽cat 𝐻𝐽 ∈ ( Subcat ‘ 𝐶 ) ) ) )
52 14 51 bitrd ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → ( 𝐽 ∈ ( Subcat ‘ 𝐷 ) ↔ ( 𝐽cat 𝐻𝐽 ∈ ( Subcat ‘ 𝐶 ) ) ) )
53 52 biancomd ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → ( 𝐽 ∈ ( Subcat ‘ 𝐷 ) ↔ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽cat 𝐻 ) ) )