Metamath Proof Explorer


Theorem rescabs2

Description: Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses rescabs2.c ( 𝜑𝐶𝑉 )
rescabs2.j ( 𝜑𝐽 Fn ( 𝑇 × 𝑇 ) )
rescabs2.s ( 𝜑𝑆𝑊 )
rescabs2.t ( 𝜑𝑇𝑆 )
Assertion rescabs2 ( 𝜑 → ( ( 𝐶s 𝑆 ) ↾cat 𝐽 ) = ( 𝐶cat 𝐽 ) )

Proof

Step Hyp Ref Expression
1 rescabs2.c ( 𝜑𝐶𝑉 )
2 rescabs2.j ( 𝜑𝐽 Fn ( 𝑇 × 𝑇 ) )
3 rescabs2.s ( 𝜑𝑆𝑊 )
4 rescabs2.t ( 𝜑𝑇𝑆 )
5 ressabs ( ( 𝑆𝑊𝑇𝑆 ) → ( ( 𝐶s 𝑆 ) ↾s 𝑇 ) = ( 𝐶s 𝑇 ) )
6 3 4 5 syl2anc ( 𝜑 → ( ( 𝐶s 𝑆 ) ↾s 𝑇 ) = ( 𝐶s 𝑇 ) )
7 6 oveq1d ( 𝜑 → ( ( ( 𝐶s 𝑆 ) ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( 𝐶s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
8 eqid ( ( 𝐶s 𝑆 ) ↾cat 𝐽 ) = ( ( 𝐶s 𝑆 ) ↾cat 𝐽 )
9 ovexd ( 𝜑 → ( 𝐶s 𝑆 ) ∈ V )
10 3 4 ssexd ( 𝜑𝑇 ∈ V )
11 8 9 10 2 rescval2 ( 𝜑 → ( ( 𝐶s 𝑆 ) ↾cat 𝐽 ) = ( ( ( 𝐶s 𝑆 ) ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
12 eqid ( 𝐶cat 𝐽 ) = ( 𝐶cat 𝐽 )
13 12 1 10 2 rescval2 ( 𝜑 → ( 𝐶cat 𝐽 ) = ( ( 𝐶s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
14 7 11 13 3eqtr4d ( 𝜑 → ( ( 𝐶s 𝑆 ) ↾cat 𝐽 ) = ( 𝐶cat 𝐽 ) )