Theorem fmptcof

Description: Version of fmptco where ph needn't be distinct from x . (Contributed by NM, 27-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		fmptcof.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 )
2		fmptcof.2	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
3		fmptcof.3	⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
4		fmptcof.4	⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
5		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝑅
6	5	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝑅 ∈ 𝐵
7		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝑅 = ⦋ 𝑧 / 𝑥 ⦌ 𝑅 )
8	7	eleq1d	⊢ ( 𝑥 = 𝑧 → ( 𝑅 ∈ 𝐵 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 ∈ 𝐵 ) )
9	6 8	rspc	⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 → ⦋ 𝑧 / 𝑥 ⦌ 𝑅 ∈ 𝐵 ) )
10	1 9	mpan9	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑥 ⦌ 𝑅 ∈ 𝐵 )
11		nfcv	⊢ Ⅎ 𝑧 𝑅
12	11 5 7	cbvmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = ( 𝑧 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 )
13	2 12	eqtrdi	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 ) )
14		nfcv	⊢ Ⅎ 𝑤 𝑆
15		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑤 / 𝑦 ⦌ 𝑆
16		csbeq1a	⊢ ( 𝑦 = 𝑤 → 𝑆 = ⦋ 𝑤 / 𝑦 ⦌ 𝑆 )
17	14 15 16	cbvmpt	⊢ ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) = ( 𝑤 ∈ 𝐵 ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑆 )
18	3 17	eqtrdi	⊢ ( 𝜑 → 𝐺 = ( 𝑤 ∈ 𝐵 ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑆 ) )
19		csbeq1	⊢ ( 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑅 → ⦋ 𝑤 / 𝑦 ⦌ 𝑆 = ⦋ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 / 𝑦 ⦌ 𝑆 )
20	10 13 18 19	fmptco	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑧 ∈ 𝐴 ↦ ⦋ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 / 𝑦 ⦌ 𝑆 ) )
21		nfcv	⊢ Ⅎ 𝑧 ⦋ 𝑅 / 𝑦 ⦌ 𝑆
22		nfcv	⊢ Ⅎ 𝑥 𝑆
23	5 22	nfcsbw	⊢ Ⅎ 𝑥 ⦋ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 / 𝑦 ⦌ 𝑆
24	7	csbeq1d	⊢ ( 𝑥 = 𝑧 → ⦋ 𝑅 / 𝑦 ⦌ 𝑆 = ⦋ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 / 𝑦 ⦌ 𝑆 )
25	21 23 24	cbvmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) = ( 𝑧 ∈ 𝐴 ↦ ⦋ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 / 𝑦 ⦌ 𝑆 )
26	20 25	eqtr4di	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) )
27		eqid	⊢ 𝐴 = 𝐴
28		nfcvd	⊢ ( 𝑅 ∈ 𝐵 → Ⅎ 𝑦 𝑇 )
29	28 4	csbiegf	⊢ ( 𝑅 ∈ 𝐵 → ⦋ 𝑅 / 𝑦 ⦌ 𝑆 = 𝑇 )
30	29	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑅 / 𝑦 ⦌ 𝑆 = 𝑇 )
31		mpteq12	⊢ ( ( 𝐴 = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ⦋ 𝑅 / 𝑦 ⦌ 𝑆 = 𝑇 ) → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )
32	27 30 31	sylancr	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )
33	1 32	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )
34	26 33	eqtrd	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )