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	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )