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 cat H
rescval2.1 φ C V
rescval2.2 φ S W
rescval2.3 φ H Fn S × S
Assertion rescval2 φ D = C 𝑠 S sSet Hom ndx H

Proof

Step Hyp Ref Expression
1 rescval.1 D = C cat H
2 rescval2.1 φ C V
3 rescval2.2 φ S W
4 rescval2.3 φ H Fn S × S
5 3 3 xpexd φ S × S V
6 fnex H Fn S × S S × S V H V
7 4 5 6 syl2anc φ H V
8 1 rescval C V H V D = C 𝑠 dom dom H sSet Hom ndx H
9 2 7 8 syl2anc φ D = C 𝑠 dom dom H sSet Hom ndx H
10 fndm H Fn S × S dom H = S × S
11 4 10 syl φ dom H = S × S
12 11 dmeqd φ dom dom H = dom S × S
13 dmxpid dom S × S = S
14 12 13 syl6eq φ dom dom H = S
15 14 oveq2d φ C 𝑠 dom dom H = C 𝑠 S
16 15 oveq1d φ C 𝑠 dom dom H sSet Hom ndx H = C 𝑠 S sSet Hom ndx H
17 9 16 eqtrd φ D = C 𝑠 S sSet Hom ndx H