# Metamath Proof Explorer

## Theorem rescabs2

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

Ref Expression
Hypotheses rescabs2.c ${⊢}{\phi }\to {C}\in {V}$
rescabs2.j ${⊢}{\phi }\to {J}Fn\left({T}×{T}\right)$
rescabs2.s ${⊢}{\phi }\to {S}\in {W}$
rescabs2.t ${⊢}{\phi }\to {T}\subseteq {S}$
Assertion rescabs2 ${⊢}{\phi }\to \left({C}{↾}_{𝑠}{S}\right){↾}_{\mathrm{cat}}{J}={C}{↾}_{\mathrm{cat}}{J}$

### Proof

Step Hyp Ref Expression
1 rescabs2.c ${⊢}{\phi }\to {C}\in {V}$
2 rescabs2.j ${⊢}{\phi }\to {J}Fn\left({T}×{T}\right)$
3 rescabs2.s ${⊢}{\phi }\to {S}\in {W}$
4 rescabs2.t ${⊢}{\phi }\to {T}\subseteq {S}$
5 ressabs ${⊢}\left({S}\in {W}\wedge {T}\subseteq {S}\right)\to \left({C}{↾}_{𝑠}{S}\right){↾}_{𝑠}{T}={C}{↾}_{𝑠}{T}$
6 3 4 5 syl2anc ${⊢}{\phi }\to \left({C}{↾}_{𝑠}{S}\right){↾}_{𝑠}{T}={C}{↾}_{𝑠}{T}$
7 6 oveq1d ${⊢}{\phi }\to \left(\left({C}{↾}_{𝑠}{S}\right){↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
8 eqid ${⊢}\left({C}{↾}_{𝑠}{S}\right){↾}_{\mathrm{cat}}{J}=\left({C}{↾}_{𝑠}{S}\right){↾}_{\mathrm{cat}}{J}$
9 ovexd ${⊢}{\phi }\to {C}{↾}_{𝑠}{S}\in \mathrm{V}$
10 3 4 ssexd ${⊢}{\phi }\to {T}\in \mathrm{V}$
11 8 9 10 2 rescval2 ${⊢}{\phi }\to \left({C}{↾}_{𝑠}{S}\right){↾}_{\mathrm{cat}}{J}=\left(\left({C}{↾}_{𝑠}{S}\right){↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
12 eqid ${⊢}{C}{↾}_{\mathrm{cat}}{J}={C}{↾}_{\mathrm{cat}}{J}$
13 12 1 10 2 rescval2 ${⊢}{\phi }\to {C}{↾}_{\mathrm{cat}}{J}=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
14 7 11 13 3eqtr4d ${⊢}{\phi }\to \left({C}{↾}_{𝑠}{S}\right){↾}_{\mathrm{cat}}{J}={C}{↾}_{\mathrm{cat}}{J}$