Theorem homaf

Description: Functionality 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 )
Assertion	homaf	⊢ ( 𝜑 → 𝐻 : ( 𝐵 × 𝐵 ) ⟶ 𝒫 ( ( 𝐵 × 𝐵 ) × V ) )

Proof

Step	Hyp	Ref	Expression
1		homarcl.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
2		homafval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		homafval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
5	1 2 3 4	homafval	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ) )
6		snssi	⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) → { 𝑥 } ⊆ ( 𝐵 × 𝐵 ) )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 × 𝐵 ) ) → { 𝑥 } ⊆ ( 𝐵 × 𝐵 ) )
8		ssv	⊢ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ⊆ V
9		xpss12	⊢ ( ( { 𝑥 } ⊆ ( 𝐵 × 𝐵 ) ∧ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ⊆ V ) → ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
10	7 8 9	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 × 𝐵 ) ) → ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
11		vsnex	⊢ { 𝑥 } ∈ V
12		fvex	⊢ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ∈ V
13	11 12	xpex	⊢ ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ V
14	13	elpw	⊢ ( ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ 𝒫 ( ( 𝐵 × 𝐵 ) × V ) ↔ ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
15	10 14	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 × 𝐵 ) ) → ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ 𝒫 ( ( 𝐵 × 𝐵 ) × V ) )
16	5 15	fmpt3d	⊢ ( 𝜑 → 𝐻 : ( 𝐵 × 𝐵 ) ⟶ 𝒫 ( ( 𝐵 × 𝐵 ) × V ) )