fdiagfn

Description: Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015)

		Ref	Expression
	Hypothesis	fdiagfn.f	$⊢ F = (x \in B ⟼ I \times \{x\})$
	Assertion	fdiagfn	$⊢ (B \in V \land I \in W) \to F : B ⟶ B^{I}$

Step	Hyp	Ref	Expression
1		fdiagfn.f	$⊢ F = (x \in B ⟼ I \times \{x\})$
2		fconst6g	$⊢ x \in B \to (I \times \{x\}) : I ⟶ B$
3	2	adantl	$⊢ ((B \in V \land I \in W) \land x \in B) \to (I \times \{x\}) : I ⟶ B$
4		elmapg	$⊢ (B \in V \land I \in W) \to (I \times \{x\} \in (B^{I}) \leftrightarrow (I \times \{x\}) : I ⟶ B)$
5	4	adantr	$⊢ ((B \in V \land I \in W) \land x \in B) \to (I \times \{x\} \in (B^{I}) \leftrightarrow (I \times \{x\}) : I ⟶ B)$
6	3 5	mpbird	$⊢ ((B \in V \land I \in W) \land x \in B) \to I \times \{x\} \in (B^{I})$
7	6 1	fmptd	$⊢ (B \in V \land I \in W) \to F : B ⟶ B^{I}$

Metamath Proof Explorer