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 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
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 𝐼 ) )