Theorem fdiagfn

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

	Ref	Expression
Hypothesis	fdiagfn.f	|- F = ( x e. B |-> ( I X. { x } ) )
Assertion	fdiagfn	|- ( ( B e. V /\ I e. W ) -> F : B --> ( B ^m I ) )

Proof

Step	Hyp	Ref	Expression
1		fdiagfn.f	|- F = ( x e. B |-> ( I X. { x } ) )
2		fconst6g	|- ( x e. B -> ( I X. { x } ) : I --> B )
3	2	adantl	|- ( ( ( B e. V /\ I e. W ) /\ x e. B ) -> ( I X. { x } ) : I --> B )
4		elmapg	|- ( ( B e. V /\ I e. W ) -> ( ( I X. { x } ) e. ( B ^m I ) <-> ( I X. { x } ) : I --> B ) )
5	4	adantr	|- ( ( ( B e. V /\ I e. W ) /\ x e. B ) -> ( ( I X. { x } ) e. ( B ^m I ) <-> ( I X. { x } ) : I --> B ) )
6	3 5	mpbird	|- ( ( ( B e. V /\ I e. W ) /\ x e. B ) -> ( I X. { x } ) e. ( B ^m I ) )
7	6 1	fmptd	|- ( ( B e. V /\ I e. W ) -> F : B --> ( B ^m I ) )