Theorem homaval

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 )
	homaval.j	⊢ 𝐽 = ( Hom ‘ 𝐶 )
	homaval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	homaval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	homaval	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( { ⟨ 𝑋 , 𝑌 ⟩ } × ( 𝑋 𝐽 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		homarcl.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
2		homafval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		homafval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		homaval.j	⊢ 𝐽 = ( Hom ‘ 𝐶 )
5		homaval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		homaval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		df-ov	⊢ ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
8	1 2 3 4	homafval	⊢ ( 𝜑 → 𝐻 = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑧 } × ( 𝐽 ‘ 𝑧 ) ) ) )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ )
10	9	sneqd	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → { 𝑧 } = { ⟨ 𝑋 , 𝑌 ⟩ } )
11	9	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
12		df-ov	⊢ ( 𝑋 𝐽 𝑌 ) = ( 𝐽 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
13	11 12	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐽 ‘ 𝑧 ) = ( 𝑋 𝐽 𝑌 ) )
14	10 13	xpeq12d	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( { 𝑧 } × ( 𝐽 ‘ 𝑧 ) ) = ( { ⟨ 𝑋 , 𝑌 ⟩ } × ( 𝑋 𝐽 𝑌 ) ) )
15	5 6	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
16		snex	⊢ { ⟨ 𝑋 , 𝑌 ⟩ } ∈ V
17		ovex	⊢ ( 𝑋 𝐽 𝑌 ) ∈ V
18	16 17	xpex	⊢ ( { ⟨ 𝑋 , 𝑌 ⟩ } × ( 𝑋 𝐽 𝑌 ) ) ∈ V
19	18	a1i	⊢ ( 𝜑 → ( { ⟨ 𝑋 , 𝑌 ⟩ } × ( 𝑋 𝐽 𝑌 ) ) ∈ V )
20	8 14 15 19	fvmptd	⊢ ( 𝜑 → ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( { ⟨ 𝑋 , 𝑌 ⟩ } × ( 𝑋 𝐽 𝑌 ) ) )
21	7 20	eqtrid	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( { ⟨ 𝑋 , 𝑌 ⟩ } × ( 𝑋 𝐽 𝑌 ) ) )