Metamath Proof Explorer

Theorem resscat

Description: A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion resscat ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐶 ↾s 𝑆 ) ∈ Cat )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
2 1 ressinbas ⊢ ( 𝑆 ∈ 𝑉 → ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) )
3 2 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) )
4 eqid ⊢ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) = ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) )
5 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
6 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → 𝐶 ∈ Cat )
7 inss2 ⊢ ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐶 )
8 7 a1i ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐶 ) )
9 1 5 6 8 fullsubc ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ∈ ( Subcat ‘ 𝐶 ) )
10 4 9 subccat ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ∈ Cat )
11 eqid ⊢ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) = ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) )
12 1 5 6 8 11 4 fullresc ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( ( Homf ‘ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) = ( Homf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) ∧ ( compf ‘ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) = ( compf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) ) )
13 12 simpld ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( Homf ‘ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) = ( Homf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) )
14 12 simprd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( compf ‘ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) = ( compf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) )
15 ovexd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ∈ V )
16 13 14 15 10 catpropd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ∈ Cat ↔ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ∈ Cat ) )
17 10 16 mpbird ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ∈ Cat )
18 3 17 eqeltrd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐶 ↾s 𝑆 ) ∈ Cat )