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		ffvelrn	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑆 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
16	2 14 15	syl2an	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
17		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
18	6 17	eqsstrri	⊢ 𝐶 ⊆ 𝐵
19	18	sseli	⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐵 )
20		ffvelrn	⊢ ( ( 𝐺 : 𝐵 ⟶ 𝑇 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑇 )
21	3 19 20	syl2an	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑇 )
22	1	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 )
24		ovrspc2v	⊢ ( ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑧 ) ∈ 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 ) → ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ∈ 𝑈 )
25	16 21 23 24	syl21anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ∈ 𝑈 )
26	11 25	fmpt3d	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) : 𝐶 ⟶ 𝑈 )