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 imbitrrid ⊢ ( 𝐻 ∈ ( 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 𝐻 ) ) )