This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) , 𝐻 ⟩ ) )