# 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}=\left({x}\in {B}⟼{I}×\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}×\left\{{x}\right\}\right)$
2 fconst6g ${⊢}{x}\in {B}\to \left({I}×\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}×\left\{{x}\right\}\right):{I}⟶{B}$
4 elmapg ${⊢}\left({B}\in {V}\wedge {I}\in {W}\right)\to \left({I}×\left\{{x}\right\}\in \left({{B}}^{{I}}\right)↔\left({I}×\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}×\left\{{x}\right\}\in \left({{B}}^{{I}}\right)↔\left({I}×\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}×\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}}$