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 𝐽 ) )