Metamath Proof Explorer

Theorem subccatid

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

Ref Expression
Hypotheses subccat.1 ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
subccat.j ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
subccatid.1 ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
subccatid.2 ⊢ 1 = ( Id ‘ 𝐶 )
Assertion subccatid ( 𝜑 → ( 𝐷 ∈ Cat ∧ ( Id ‘ 𝐷 ) = ( 𝑥 ∈ 𝑆 ↦ ( 1 ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 subccat.1 ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
2 subccat.j ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
3 subccatid.1 ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
4 subccatid.2 ⊢ 1 = ( Id ‘ 𝐶 )
5 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 subcrcl ⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat )
7 2 6 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
8 2 3 5 subcss1 ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐶 ) )
9 1 5 7 3 8 rescbas ⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐷 ) )
10 1 5 7 3 8 reschom ⊢ ( 𝜑 → 𝐽 = ( Hom ‘ 𝐷 ) )
11 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
12 1 5 7 3 8 11 rescco ⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐷 ) )
13 1 ovexi ⊢ 𝐷 ∈ V
14 13 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
15 biid ⊢ ( ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ↔ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) )
16 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
17 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐽 Fn ( 𝑆 × 𝑆 ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
19 16 17 18 4 subcidcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
20 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
21 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝐶 ∈ Cat )
22 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑆 ⊆ ( Base ‘ 𝐶 ) )
23 simpr1l ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑤 ∈ 𝑆 )
24 22 23 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
25 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑥 ∈ 𝑆 )
26 22 25 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
27 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
28 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝐽 Fn ( 𝑆 × 𝑆 ) )
29 27 28 20 23 25 subcss2 ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑤 𝐽 𝑥 ) ⊆ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) )
30 simpr31 ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) )
31 29 30 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) )
32 5 20 4 21 24 11 26 31 catlid ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 )
33 simpr2l ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑦 ∈ 𝑆 )
34 22 33 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
35 27 28 20 25 33 subcss2 ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑥 𝐽 𝑦 ) ⊆ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
36 simpr32 ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) )
37 35 36 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
38 5 20 4 21 26 11 34 37 catrid ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( 1 ‘ 𝑥 ) ) = 𝑔 )
39 27 28 23 11 25 33 30 36 subccocl ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ∈ ( 𝑤 𝐽 𝑦 ) )
40 simpr2r ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑧 ∈ 𝑆 )
41 22 40 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
42 27 28 20 33 40 subcss2 ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑦 𝐽 𝑧 ) ⊆ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
43 simpr33 ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ℎ ∈ ( 𝑦 𝐽 𝑧 ) )
44 42 43 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ℎ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
45 5 20 11 21 24 26 34 31 37 41 44 catass ⊢ ( ( 𝜑 ∧ ( ( 𝑤 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑤 𝐽 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 𝐽 𝑦 ) ∧ ℎ ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( ( ℎ ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ℎ ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) )
46 9 10 12 14 15 19 32 38 39 45 iscatd2 ⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ ( Id ‘ 𝐷 ) = ( 𝑥 ∈ 𝑆 ↦ ( 1 ‘ 𝑥 ) ) ) )