Metamath Proof Explorer


Theorem rescval

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

Ref Expression
Hypothesis rescval.1 𝐷 = ( 𝐶cat 𝐻 )
Assertion rescval ( ( 𝐶𝑉𝐻𝑊 ) → 𝐷 = ( ( 𝐶s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )

Proof

Step Hyp Ref Expression
1 rescval.1 𝐷 = ( 𝐶cat 𝐻 )
2 elex ( 𝐶𝑉𝐶 ∈ V )
3 elex ( 𝐻𝑊𝐻 ∈ V )
4 simpl ( ( 𝑐 = 𝐶 = 𝐻 ) → 𝑐 = 𝐶 )
5 simpr ( ( 𝑐 = 𝐶 = 𝐻 ) → = 𝐻 )
6 5 dmeqd ( ( 𝑐 = 𝐶 = 𝐻 ) → dom = dom 𝐻 )
7 6 dmeqd ( ( 𝑐 = 𝐶 = 𝐻 ) → dom dom = dom dom 𝐻 )
8 4 7 oveq12d ( ( 𝑐 = 𝐶 = 𝐻 ) → ( 𝑐s dom dom ) = ( 𝐶s dom dom 𝐻 ) )
9 5 opeq2d ( ( 𝑐 = 𝐶 = 𝐻 ) → ⟨ ( Hom ‘ ndx ) , ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ )
10 8 9 oveq12d ( ( 𝑐 = 𝐶 = 𝐻 ) → ( ( 𝑐s dom dom ) sSet ⟨ ( Hom ‘ ndx ) , ⟩ ) = ( ( 𝐶s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
11 df-resc cat = ( 𝑐 ∈ V , ∈ V ↦ ( ( 𝑐s dom dom ) sSet ⟨ ( Hom ‘ ndx ) , ⟩ ) )
12 ovex ( ( 𝐶s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ∈ V
13 10 11 12 ovmpoa ( ( 𝐶 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐶cat 𝐻 ) = ( ( 𝐶s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
14 2 3 13 syl2an ( ( 𝐶𝑉𝐻𝑊 ) → ( 𝐶cat 𝐻 ) = ( ( 𝐶s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
15 1 14 eqtrid ( ( 𝐶𝑉𝐻𝑊 ) → 𝐷 = ( ( 𝐶s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )