Theorem homaf

Description: Functionality 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 )
Assertion	homaf	|- ( ph -> H : ( B X. B ) --> ~P ( ( B X. B ) X. _V ) )

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		eqid	|- ( Hom ` C ) = ( Hom ` C )
5	1 2 3 4	homafval	|- ( ph -> H = ( x e. ( B X. B ) |-> ( { x } X. ( ( Hom ` C ) ` x ) ) ) )
6		snssi	|- ( x e. ( B X. B ) -> { x } C_ ( B X. B ) )
7	6	adantl	|- ( ( ph /\ x e. ( B X. B ) ) -> { x } C_ ( B X. B ) )
8		ssv	|- ( ( Hom ` C ) ` x ) C_ _V
9		xpss12	|- ( ( { x } C_ ( B X. B ) /\ ( ( Hom ` C ) ` x ) C_ _V ) -> ( { x } X. ( ( Hom ` C ) ` x ) ) C_ ( ( B X. B ) X. _V ) )
10	7 8 9	sylancl	|- ( ( ph /\ x e. ( B X. B ) ) -> ( { x } X. ( ( Hom ` C ) ` x ) ) C_ ( ( B X. B ) X. _V ) )
11		snex	|- { x } e. _V
12		fvex	|- ( ( Hom ` C ) ` x ) e. _V
13	11 12	xpex	|- ( { x } X. ( ( Hom ` C ) ` x ) ) e. _V
14	13	elpw	|- ( ( { x } X. ( ( Hom ` C ) ` x ) ) e. ~P ( ( B X. B ) X. _V ) <-> ( { x } X. ( ( Hom ` C ) ` x ) ) C_ ( ( B X. B ) X. _V ) )
15	10 14	sylibr	|- ( ( ph /\ x e. ( B X. B ) ) -> ( { x } X. ( ( Hom ` C ) ` x ) ) e. ~P ( ( B X. B ) X. _V ) )
16	5 15	fmpt3d	|- ( ph -> H : ( B X. B ) --> ~P ( ( B X. B ) X. _V ) )