Theorem mpomptsx

Description: Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	mpomptsx	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑢 ∈ V
2		vex	⊢ 𝑣 ∈ V
3	1 2	op1std	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st ‘ 𝑧 ) = 𝑢 )
4	3	csbeq1d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
5	1 2	op2ndd	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑣 )
6	5	csbeq1d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
7	6	csbeq2dv	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ 𝑢 / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
8	4 7	eqtrd	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
9	8	mpomptx	⊢ ( 𝑧 ∈ ∪ 𝑢 ∈ 𝐴 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
10		nfcv	⊢ Ⅎ 𝑢 ( { 𝑥 } × 𝐵 )
11		nfcv	⊢ Ⅎ 𝑥 { 𝑢 }
12		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ 𝐵
13	11 12	nfxp	⊢ Ⅎ 𝑥 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 )
14		sneq	⊢ ( 𝑥 = 𝑢 → { 𝑥 } = { 𝑢 } )
15		csbeq1a	⊢ ( 𝑥 = 𝑢 → 𝐵 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 )
16	14 15	xpeq12d	⊢ ( 𝑥 = 𝑢 → ( { 𝑥 } × 𝐵 ) = ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) )
17	10 13 16	cbviun	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ∪ 𝑢 ∈ 𝐴 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 )
18	17	mpteq1i	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ) = ( 𝑧 ∈ ∪ 𝑢 ∈ 𝐴 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
19		nfcv	⊢ Ⅎ 𝑢 𝐵
20		nfcv	⊢ Ⅎ 𝑢 𝐶
21		nfcv	⊢ Ⅎ 𝑣 𝐶
22		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶
23		nfcv	⊢ Ⅎ 𝑦 𝑢
24		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑦 ⦌ 𝐶
25	23 24	nfcsbw	⊢ Ⅎ 𝑦 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶
26		csbeq1a	⊢ ( 𝑦 = 𝑣 → 𝐶 = ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
27		csbeq1a	⊢ ( 𝑥 = 𝑢 → ⦋ 𝑣 / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
28	26 27	sylan9eqr	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
29	19 12 20 21 22 25 15 28	cbvmpox	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
30	9 18 29	3eqtr4ri	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )