Theorem ofcf

Description: The function/constant operation produces a function. (Contributed by Thierry Arnoux, 30-Jan-2017)

	Ref	Expression
Hypotheses	ofcf.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇 ) ) → ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 )
	ofcf.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	ofcf.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofcf.5	⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
Assertion	ofcf	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) : 𝐴 ⟶ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		ofcf.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇 ) ) → ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 )
2		ofcf.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3		ofcf.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		ofcf.5	⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
5	2	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
6		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
7	5 3 4 6	ofcfval	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) 𝑅 𝐶 ) ) )
8	2	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
9	4	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ 𝑇 )
10	1	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 )
12		ovrspc2v	⊢ ( ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 𝑅 𝑦 ) ∈ 𝑈 ) → ( ( 𝐹 ‘ 𝑧 ) 𝑅 𝐶 ) ∈ 𝑈 )
13	8 9 11 12	syl21anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) 𝑅 𝐶 ) ∈ 𝑈 )
14	7 13	fmpt3d	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) : 𝐴 ⟶ 𝑈 )