off2

Description: The function operation produces a function - alternative form with all antecedents as deduction. (Contributed by Thierry Arnoux, 17-Feb-2017)

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

Proof

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

Metamath Proof Explorer

Theorem off2

Proof