This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )