homaf

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

	Ref	Expression
Hypotheses	homarcl.h	$⊢ H = {Hom}_{a} (C)$
	homafval.b	$⊢ B = {Base}_{C}$
	homafval.c	$⊢ φ \to C \in Cat$
Assertion	homaf	$⊢ φ \to H : B \times B ⟶ 𝒫 ((B \times B) \times V)$

Step	Hyp	Ref	Expression
1		homarcl.h	$⊢ H = {Hom}_{a} (C)$
2		homafval.b	$⊢ B = {Base}_{C}$
3		homafval.c	$⊢ φ \to C \in Cat$
4		eqid	$⊢ Hom (C) = Hom (C)$
5	1 2 3 4	homafval	$⊢ φ \to H = (x \in (B \times B) ⟼ \{x\} \times Hom (C) (x))$
6		snssi	$⊢ x \in (B \times B) \to \{x\} \subseteq B \times B$
7	6	adantl	$⊢ (φ \land x \in (B \times B)) \to \{x\} \subseteq B \times B$
8		ssv	$⊢ Hom (C) (x) \subseteq V$
9		xpss12	$⊢ (\{x\} \subseteq B \times B \land Hom (C) (x) \subseteq V) \to \{x\} \times Hom (C) (x) \subseteq (B \times B) \times V$
10	7 8 9	sylancl	$⊢ (φ \land x \in (B \times B)) \to \{x\} \times Hom (C) (x) \subseteq (B \times B) \times V$
11		vsnex	$⊢ \{x\} \in V$
12		fvex	$⊢ Hom (C) (x) \in V$
13	11 12	xpex	$⊢ \{x\} \times Hom (C) (x) \in V$
14	13	elpw	$⊢ \{x\} \times Hom (C) (x) \in 𝒫 ((B \times B) \times V) \leftrightarrow \{x\} \times Hom (C) (x) \subseteq (B \times B) \times V$
15	10 14	sylibr	$⊢ (φ \land x \in (B \times B)) \to \{x\} \times Hom (C) (x) \in 𝒫 ((B \times B) \times V)$
16	5 15	fmpt3d	$⊢ φ \to H : B \times B ⟶ 𝒫 ((B \times B) \times V)$

Metamath Proof Explorer