Theorem reschomf

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	reschomf	⊢ ( 𝜑 → 𝐻 = ( Homf ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		rescbas.d	⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
2		rescbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		rescbas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		rescbas.h	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
5		rescbas.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
6	1 2 3 4 5	reschom	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐷 ) )
7	1 2 3 4 5	rescbas	⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐷 ) )
8	7	sqxpeqd	⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) = ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
9	6 8	fneq12d	⊢ ( 𝜑 → ( 𝐻 Fn ( 𝑆 × 𝑆 ) ↔ ( Hom ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ) )
10	4 9	mpbid	⊢ ( 𝜑 → ( Hom ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
11		fnov	⊢ ( ( Hom ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↔ ( Hom ‘ 𝐷 ) = ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
12	10 11	sylib	⊢ ( 𝜑 → ( Hom ‘ 𝐷 ) = ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
13	6 12	eqtrd	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
14		eqid	⊢ ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐷 )
15		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
16		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
17	14 15 16	homffval	⊢ ( Homf ‘ 𝐷 ) = ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
18	13 17	eqtr4di	⊢ ( 𝜑 → 𝐻 = ( Homf ‘ 𝐷 ) )