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 ⊢ φ → C ∈ V
rescabs2.j ⊢ φ → J Fn T × T
rescabs2.s ⊢ φ → S ∈ W
rescabs2.t ⊢ φ → T ⊆ S
Assertion rescabs2 ⊢ φ → C ↾ 𝑠 S ↾ cat J = C ↾ cat J

Proof

Step Hyp Ref Expression
1 rescabs2.c ⊢ φ → C ∈ V
2 rescabs2.j ⊢ φ → J Fn T × T
3 rescabs2.s ⊢ φ → S ∈ W
4 rescabs2.t ⊢ φ → T ⊆ S
5 ressabs ⊢ S ∈ W ∧ T ⊆ S → C ↾ 𝑠 S ↾ 𝑠 T = C ↾ 𝑠 T
6 3 4 5 syl2anc ⊢ φ → C ↾ 𝑠 S ↾ 𝑠 T = C ↾ 𝑠 T
7 6 oveq1d ⊢ φ → C ↾ 𝑠 S ↾ 𝑠 T sSet Hom ⁡ ndx J = C ↾ 𝑠 T sSet Hom ⁡ ndx J
8 eqid ⊢ C ↾ 𝑠 S ↾ cat J = C ↾ 𝑠 S ↾ cat J
9 ovexd ⊢ φ → C ↾ 𝑠 S ∈ V
10 3 4 ssexd ⊢ φ → T ∈ V
11 8 9 10 2 rescval2 ⊢ φ → C ↾ 𝑠 S ↾ cat J = C ↾ 𝑠 S ↾ 𝑠 T sSet Hom ⁡ ndx J
12 eqid ⊢ C ↾ cat J = C ↾ cat J
13 12 1 10 2 rescval2 ⊢ φ → C ↾ cat J = C ↾ 𝑠 T sSet Hom ⁡ ndx J
14 7 11 13 3eqtr4d ⊢ φ → C ↾ 𝑠 S ↾ cat J = C ↾ cat J