Theorem elhoma

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

	Ref	Expression
Hypotheses	homarcl.h	|- H = ( HomA ` C )
	homafval.b	|- B = ( Base ` C )
	homafval.c	|- ( ph -> C e. Cat )
	homaval.j	|- J = ( Hom ` C )
	homaval.x	|- ( ph -> X e. B )
	homaval.y	|- ( ph -> Y e. B )
Assertion	elhoma	|- ( ph -> ( Z ( X H Y ) F <-> ( Z = <. X , Y >. /\ F e. ( X J Y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		homarcl.h	|- H = ( HomA ` C )
2		homafval.b	|- B = ( Base ` C )
3		homafval.c	|- ( ph -> C e. Cat )
4		homaval.j	|- J = ( Hom ` C )
5		homaval.x	|- ( ph -> X e. B )
6		homaval.y	|- ( ph -> Y e. B )
7	1 2 3 4 5 6	homaval	|- ( ph -> ( X H Y ) = ( { <. X , Y >. } X. ( X J Y ) ) )
8	7	breqd	|- ( ph -> ( Z ( X H Y ) F <-> Z ( { <. X , Y >. } X. ( X J Y ) ) F ) )
9		brxp	|- ( Z ( { <. X , Y >. } X. ( X J Y ) ) F <-> ( Z e. { <. X , Y >. } /\ F e. ( X J Y ) ) )
10		opex	|- <. X , Y >. e. _V
11	10	elsn2	|- ( Z e. { <. X , Y >. } <-> Z = <. X , Y >. )
12	11	anbi1i	|- ( ( Z e. { <. X , Y >. } /\ F e. ( X J Y ) ) <-> ( Z = <. X , Y >. /\ F e. ( X J Y ) ) )
13	9 12	bitri	|- ( Z ( { <. X , Y >. } X. ( X J Y ) ) F <-> ( Z = <. X , Y >. /\ F e. ( X J Y ) ) )
14	8 13	bitrdi	|- ( ph -> ( Z ( X H Y ) F <-> ( Z = <. X , Y >. /\ F e. ( X J Y ) ) ) )