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

Metamath Proof Explorer

Theorem reschom

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

Ref Expression
Hypotheses rescbas.d ⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
rescbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
rescbas.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
rescbas.h ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
rescbas.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion reschom ( 𝜑 → 𝐻 = ( Hom ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 rescbas.d ⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
2 rescbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 rescbas.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 rescbas.h ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
5 rescbas.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
6 ovex ⊢ ( 𝐶 ↾s 𝑆 ) ∈ V
7 2 fvexi ⊢ 𝐵 ∈ V
8 7 ssex ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 ∈ V )
9 5 8 syl ⊢ ( 𝜑 → 𝑆 ∈ V )
10 9 9 xpexd ⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) ∈ V )
11 fnex ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝑆 × 𝑆 ) ∈ V ) → 𝐻 ∈ V )
12 4 10 11 syl2anc ⊢ ( 𝜑 → 𝐻 ∈ V )
13 homid ⊢ Hom = Slot ( Hom ‘ ndx )
14 13 setsid ⊢ ( ( ( 𝐶 ↾s 𝑆 ) ∈ V ∧ 𝐻 ∈ V ) → 𝐻 = ( Hom ‘ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ) )
15 6 12 14 sylancr ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ) )
16 1 3 9 4 rescval2 ⊢ ( 𝜑 → 𝐷 = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
17 16 fveq2d ⊢ ( 𝜑 → ( Hom ‘ 𝐷 ) = ( Hom ‘ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ) )
18 15 17 eqtr4d ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐷 ) )