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

Metamath Proof Explorer

Theorem fmpt2d

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014)

Ref Expression
Hypotheses fmpt2d.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
fmpt2d.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
fmpt2d.3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐶 )
Assertion fmpt2d ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )

Proof

Step Hyp Ref Expression
1 fmpt2d.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 fmpt2d.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
3 fmpt2d.3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐶 )
4 1 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
5 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6 5 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
7 4 6 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
8 2 fneq1d ⊢ ( 𝜑 → ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ) )
9 7 8 mpbird ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
10 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝐶 )
11 ffnfv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝐶 ) )
12 9 10 11 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )