# Metamath Proof Explorer

## Theorem rescval2

Description: Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses rescval.1 ${⊢}{D}={C}{↾}_{\mathrm{cat}}{H}$
rescval2.1 ${⊢}{\phi }\to {C}\in {V}$
rescval2.2 ${⊢}{\phi }\to {S}\in {W}$
rescval2.3 ${⊢}{\phi }\to {H}Fn\left({S}×{S}\right)$
Assertion rescval2 ${⊢}{\phi }\to {D}=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$

### Proof

Step Hyp Ref Expression
1 rescval.1 ${⊢}{D}={C}{↾}_{\mathrm{cat}}{H}$
2 rescval2.1 ${⊢}{\phi }\to {C}\in {V}$
3 rescval2.2 ${⊢}{\phi }\to {S}\in {W}$
4 rescval2.3 ${⊢}{\phi }\to {H}Fn\left({S}×{S}\right)$
5 3 3 xpexd ${⊢}{\phi }\to {S}×{S}\in \mathrm{V}$
6 fnex ${⊢}\left({H}Fn\left({S}×{S}\right)\wedge {S}×{S}\in \mathrm{V}\right)\to {H}\in \mathrm{V}$
7 4 5 6 syl2anc ${⊢}{\phi }\to {H}\in \mathrm{V}$
8 1 rescval ${⊢}\left({C}\in {V}\wedge {H}\in \mathrm{V}\right)\to {D}=\left({C}{↾}_{𝑠}\mathrm{dom}\mathrm{dom}{H}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
9 2 7 8 syl2anc ${⊢}{\phi }\to {D}=\left({C}{↾}_{𝑠}\mathrm{dom}\mathrm{dom}{H}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
10 fndm ${⊢}{H}Fn\left({S}×{S}\right)\to \mathrm{dom}{H}={S}×{S}$
11 4 10 syl ${⊢}{\phi }\to \mathrm{dom}{H}={S}×{S}$
12 11 dmeqd ${⊢}{\phi }\to \mathrm{dom}\mathrm{dom}{H}=\mathrm{dom}\left({S}×{S}\right)$
13 dmxpid ${⊢}\mathrm{dom}\left({S}×{S}\right)={S}$
14 12 13 syl6eq ${⊢}{\phi }\to \mathrm{dom}\mathrm{dom}{H}={S}$
15 14 oveq2d ${⊢}{\phi }\to {C}{↾}_{𝑠}\mathrm{dom}\mathrm{dom}{H}={C}{↾}_{𝑠}{S}$
16 15 oveq1d ${⊢}{\phi }\to \left({C}{↾}_{𝑠}\mathrm{dom}\mathrm{dom}{H}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
17 9 16 eqtrd ${⊢}{\phi }\to {D}=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$