Metamath Proof Explorer

Theorem rescval

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

Ref Expression
Hypothesis rescval.1 ⊢ D = C ↾ cat H
Assertion rescval ⊢ C ∈ V ∧ H ∈ W → D = C ↾ 𝑠 dom ⁡ dom ⁡ H sSet Hom ⁡ ndx H

Proof

Step Hyp Ref Expression
1 rescval.1 ⊢ D = C ↾ cat H
2 elex ⊢ C ∈ V → C ∈ V
3 elex ⊢ H ∈ W → H ∈ V
4 simpl ⊢ c = C ∧ h = H → c = C
5 simpr ⊢ c = C ∧ h = H → h = H
6 5 dmeqd ⊢ c = C ∧ h = H → dom ⁡ h = dom ⁡ H
7 6 dmeqd ⊢ c = C ∧ h = H → dom ⁡ dom ⁡ h = dom ⁡ dom ⁡ H
8 4 7 oveq12d ⊢ c = C ∧ h = H → c ↾ 𝑠 dom ⁡ dom ⁡ h = C ↾ 𝑠 dom ⁡ dom ⁡ H
9 5 opeq2d ⊢ c = C ∧ h = H → Hom ⁡ ndx h = Hom ⁡ ndx H
10 8 9 oveq12d ⊢ c = C ∧ h = H → c ↾ 𝑠 dom ⁡ dom ⁡ h sSet Hom ⁡ ndx h = C ↾ 𝑠 dom ⁡ dom ⁡ H sSet Hom ⁡ ndx H
11 df-resc ⊢ ↾ cat = c ∈ V , h ∈ V ⟼ c ↾ 𝑠 dom ⁡ dom ⁡ h sSet Hom ⁡ ndx h
12 ovex ⊢ C ↾ 𝑠 dom ⁡ dom ⁡ H sSet Hom ⁡ ndx H ∈ V
13 10 11 12 ovmpoa ⊢ C ∈ V ∧ H ∈ V → C ↾ cat H = C ↾ 𝑠 dom ⁡ dom ⁡ H sSet Hom ⁡ ndx H
14 2 3 13 syl2an ⊢ C ∈ V ∧ H ∈ W → C ↾ cat H = C ↾ 𝑠 dom ⁡ dom ⁡ H sSet Hom ⁡ ndx H
15 1 14 eqtrid ⊢ C ∈ V ∧ H ∈ W → D = C ↾ 𝑠 dom ⁡ dom ⁡ H sSet Hom ⁡ ndx H