Theorem fmpocos

Description: Composition of two functions. Variation of fmpoco with more context in the substitution hypothesis for T . (Contributed by SN, 14-Mar-2025)

	Ref	Expression
Hypotheses	fmpocos.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑅 ∈ 𝐶 )
	fmpocos.2	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) )
	fmpocos.3	⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ 𝐶 ↦ 𝑆 ) )
	fmpocos.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ⦋ 𝑅 / 𝑧 ⦌ 𝑆 = 𝑇 )
Assertion	fmpocos	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		fmpocos.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑅 ∈ 𝐶 )
2		fmpocos.2	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) )
3		fmpocos.3	⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ 𝐶 ↦ 𝑆 ) )
4		fmpocos.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ⦋ 𝑅 / 𝑧 ⦌ 𝑆 = 𝑇 )
5	1	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑅 ∈ 𝐶 )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 )
7	6	fmpo	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑅 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
8	5 7	sylib	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
9		nfcv	⊢ Ⅎ 𝑢 𝑅
10		nfcv	⊢ Ⅎ 𝑣 𝑅
11		nfcv	⊢ Ⅎ 𝑥 𝑣
12		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ 𝑅
13	11 12	nfcsbw	⊢ Ⅎ 𝑥 ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅
14		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅
15		csbeq1a	⊢ ( 𝑥 = 𝑢 → 𝑅 = ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
16		csbeq1a	⊢ ( 𝑦 = 𝑣 → ⦋ 𝑢 / 𝑥 ⦌ 𝑅 = ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
17	15 16	sylan9eq	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑅 = ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
18	9 10 13 14 17	cbvmpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
19		vex	⊢ 𝑢 ∈ V
20		vex	⊢ 𝑣 ∈ V
21	19 20	op2ndd	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd ‘ 𝑤 ) = 𝑣 )
22	19 20	op1std	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st ‘ 𝑤 ) = 𝑢 )
23	22	csbeq1d	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 = ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
24	21 23	csbeq12dv	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 = ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
25	24	mpompt	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
26	18 25	eqtr4i	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 )
27	26	fmpt	⊢ ( ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
28	8 27	sylibr	⊢ ( 𝜑 → ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ∈ 𝐶 )
29	2 26	eqtrdi	⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ) )
30	28 29 3	fmptcos	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) )
31	24	csbeq1d	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 = ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
32	31	mpompt	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
33		nfcv	⊢ Ⅎ 𝑢 ⦋ 𝑅 / 𝑧 ⦌ 𝑆
34		nfcv	⊢ Ⅎ 𝑣 ⦋ 𝑅 / 𝑧 ⦌ 𝑆
35		nfcv	⊢ Ⅎ 𝑥 𝑆
36	13 35	nfcsbw	⊢ Ⅎ 𝑥 ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆
37		nfcv	⊢ Ⅎ 𝑦 𝑆
38	14 37	nfcsbw	⊢ Ⅎ 𝑦 ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆
39	17	csbeq1d	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ⦋ 𝑅 / 𝑧 ⦌ 𝑆 = ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
40	33 34 36 38 39	cbvmpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⦋ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
41	32 40	eqtr4i	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⦋ 𝑅 / 𝑧 ⦌ 𝑆 )
42	4	3impb	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑅 / 𝑧 ⦌ 𝑆 = 𝑇 )
43	42	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⦋ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )
44	41 43	eqtrid	⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )
45	30 44	eqtrd	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )