Theorem offn

Description: The function operation produces a function. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypotheses	offval.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	offval.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
	offval.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	offval.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	offval.5	⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆
Assertion	offn	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) Fn 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		offval.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		offval.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
3		offval.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		offval.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5		offval.5	⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆
6		ovex	⊢ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ∈ V
7		eqid	⊢ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
8	6 7	fnmpti	⊢ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) Fn 𝑆
9		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
10		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
11	1 2 3 4 5 9 10	offval	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
12	11	fneq1d	⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) Fn 𝑆 ↔ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) Fn 𝑆 ) )
13	8 12	mpbiri	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) Fn 𝑆 )