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

Metamath Proof Explorer

Theorem off

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

Ref Expression
Hypotheses off.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇 ) ) → ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 )
off.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
off.3 ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝑇 )
off.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
off.5 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
off.6 ⊢ ( 𝐴 ∩ 𝐵 ) = 𝐶
Assertion off ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) : 𝐶 ⟶ 𝑈 )

Proof

Step Hyp Ref Expression
1 off.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇 ) ) → ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 )
2 off.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3 off.3 ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝑇 )
4 off.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 off.5 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
6 off.6 ⊢ ( 𝐴 ∩ 𝐵 ) = 𝐶
7 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
8 3 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
9 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
10 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
11 7 8 4 5 6 9 10 offval ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑧 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ) )
12 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
13 6 12 eqsstrri ⊢ 𝐶 ⊆ 𝐴
14 13 sseli ⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐴 )
15 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑆 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
16 2 14 15 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
17 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
18 6 17 eqsstrri ⊢ 𝐶 ⊆ 𝐵
19 18 sseli ⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐵 )
20 ffvelcdm ⊢ ( ( 𝐺 : 𝐵 ⟶ 𝑇 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑇 )
21 3 19 20 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑇 )
22 1 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 )
24 ovrspc2v ⊢ ( ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑧 ) ∈ 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 ) → ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ∈ 𝑈 )
25 16 21 23 24 syl21anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ∈ 𝑈 )
26 11 25 fmpt3d ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) : 𝐶 ⟶ 𝑈 )