Theorem fdiagfn

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

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

Proof

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