This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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