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 ‘ 𝐷 ) )