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

Metamath Proof Explorer

Theorem rescval2

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

Ref Expression
Hypotheses rescval.1 ⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
rescval2.1 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
rescval2.2 ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
rescval2.3 ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
Assertion rescval2 ( 𝜑 → 𝐷 = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )

Proof

Step Hyp Ref Expression
1 rescval.1 ⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
2 rescval2.1 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
3 rescval2.2 ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
4 rescval2.3 ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
5 3 3 xpexd ⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) ∈ V )
6 fnex ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝑆 × 𝑆 ) ∈ V ) → 𝐻 ∈ V )
7 4 5 6 syl2anc ⊢ ( 𝜑 → 𝐻 ∈ V )
8 1 rescval ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐻 ∈ V ) → 𝐷 = ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
9 2 7 8 syl2anc ⊢ ( 𝜑 → 𝐷 = ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
10 4 fndmd ⊢ ( 𝜑 → dom 𝐻 = ( 𝑆 × 𝑆 ) )
11 10 dmeqd ⊢ ( 𝜑 → dom dom 𝐻 = dom ( 𝑆 × 𝑆 ) )
12 dmxpid ⊢ dom ( 𝑆 × 𝑆 ) = 𝑆
13 11 12 eqtrdi ⊢ ( 𝜑 → dom dom 𝐻 = 𝑆 )
14 13 oveq2d ⊢ ( 𝜑 → ( 𝐶 ↾s dom dom 𝐻 ) = ( 𝐶 ↾s 𝑆 ) )
15 14 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
16 9 15 eqtrd ⊢ ( 𝜑 → 𝐷 = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )