Theorem fdiagfn

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

	Ref	Expression
Hypothesis	fdiagfn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
Assertion	fdiagfn	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 : 𝐵 ⟶ ( 𝐵 ↑m 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		fdiagfn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
2		fconst6g	⊢ ( 𝑥 ∈ 𝐵 → ( 𝐼 × { 𝑥 } ) : 𝐼 ⟶ 𝐵 )
3	2	adantl	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 × { 𝑥 } ) : 𝐼 ⟶ 𝐵 )
4		elmapg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( 𝐼 × { 𝑥 } ) ∈ ( 𝐵 ↑m 𝐼 ) ↔ ( 𝐼 × { 𝑥 } ) : 𝐼 ⟶ 𝐵 ) )
5	4	adantr	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐼 × { 𝑥 } ) ∈ ( 𝐵 ↑m 𝐼 ) ↔ ( 𝐼 × { 𝑥 } ) : 𝐼 ⟶ 𝐵 ) )
6	3 5	mpbird	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 × { 𝑥 } ) ∈ ( 𝐵 ↑m 𝐼 ) )
7	6 1	fmptd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 : 𝐵 ⟶ ( 𝐵 ↑m 𝐼 ) )