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 B I × x
Assertion fdiagfn B V I W F : B B I

Proof

Step Hyp Ref Expression
1 fdiagfn.f F = x B I × x
2 fconst6g x B I × x : I B
3 2 adantl B V I W x B I × x : I B
4 elmapg B V I W I × x B I I × x : I B
5 4 adantr B V I W x B I × x B I I × x : I B
6 3 5 mpbird B V I W x B I × x B I
7 6 1 fmptd B V I W F : B B I