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

Metamath Proof Explorer

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 𝑆 )