Theorem homafval

Description: Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	homarcl.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
	homafval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	homafval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	homafval.j	⊢ 𝐽 = ( Hom ‘ 𝐶 )
Assertion	homafval	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		homarcl.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
2		homafval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		homafval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		homafval.j	⊢ 𝐽 = ( Hom ‘ 𝐶 )
5		fveq2	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
6	5 2	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
7	6	sqxpeqd	⊢ ( 𝑐 = 𝐶 → ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) = ( 𝐵 × 𝐵 ) )
8		fveq2	⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
9	8 4	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = 𝐽 )
10	9	fveq1d	⊢ ( 𝑐 = 𝐶 → ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) = ( 𝐽 ‘ 𝑥 ) )
11	10	xpeq2d	⊢ ( 𝑐 = 𝐶 → ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) = ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) )
12	7 11	mpteq12dv	⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) )
13		df-homa	⊢ Homa = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) )
14	2	fvexi	⊢ 𝐵 ∈ V
15	14 14	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
16	15	mptex	⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) ∈ V
17	12 13 16	fvmpt	⊢ ( 𝐶 ∈ Cat → ( Homa ‘ 𝐶 ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) )
18	3 17	syl	⊢ ( 𝜑 → ( Homa ‘ 𝐶 ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) )
19	1 18	syl5eq	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) )