Theorem fvdiagfn

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	fvdiagfn	$$⊢\left(I\in W\wedge X\in B\right)\to F\left(X\right)=I\times \left\{X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fdiagfn.f	$$⊢F=\left(x\in B⟼I\times \left\{x\right\}\right)$$
2		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
3	2	xpeq2d	$$⊢x=X\to I\times \left\{x\right\}=I\times \left\{X\right\}$$
4		simpr	$$⊢\left(I\in W\wedge X\in B\right)\to X\in B$$
5		snex	$$⊢\left\{X\right\}\in \mathrm{V}$$
6		xpexg	$$⊢\left(I\in W\wedge \left\{X\right\}\in \mathrm{V}\right)\to I\times \left\{X\right\}\in \mathrm{V}$$
7	5 6	mpan2	$$⊢I\in W\to I\times \left\{X\right\}\in \mathrm{V}$$
8	7	adantr	$$⊢\left(I\in W\wedge X\in B\right)\to I\times \left\{X\right\}\in \mathrm{V}$$
9	1 3 4 8	fvmptd3	$$⊢\left(I\in W\wedge X\in B\right)\to F\left(X\right)=I\times \left\{X\right\}$$