Theorem fmptcos

Description: Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	fmptcof.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 )
	fmptcof.2	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
	fmptcof.3	⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
Assertion	fmptcos	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		fmptcof.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 )
2		fmptcof.2	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
3		fmptcof.3	⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
4		nfcv	⊢ Ⅎ 𝑧 𝑆
5		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑦 ⦌ 𝑆
6		csbeq1a	⊢ ( 𝑦 = 𝑧 → 𝑆 = ⦋ 𝑧 / 𝑦 ⦌ 𝑆 )
7	4 5 6	cbvmpt	⊢ ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) = ( 𝑧 ∈ 𝐵 ↦ ⦋ 𝑧 / 𝑦 ⦌ 𝑆 )
8	3 7	eqtrdi	⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ 𝐵 ↦ ⦋ 𝑧 / 𝑦 ⦌ 𝑆 ) )
9		csbeq1	⊢ ( 𝑧 = 𝑅 → ⦋ 𝑧 / 𝑦 ⦌ 𝑆 = ⦋ 𝑅 / 𝑦 ⦌ 𝑆 )
10	1 2 8 9	fmptcof	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) )