Theorem mpocurryd

Description: The currying of an operation given in maps-to notation, splitting the operation (function of two arguments) into a function of the first argument, producing a function over the second argument. (Contributed by AV, 27-Oct-2019)

	Ref	Expression
Hypotheses	mpocurryd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
	mpocurryd.c	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 )
	mpocurryd.n	⊢ ( 𝜑 → 𝑌 ≠ ∅ )
Assertion	mpocurryd	⊢ ( 𝜑 → curry 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mpocurryd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
2		mpocurryd.c	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 )
3		mpocurryd.n	⊢ ( 𝜑 → 𝑌 ≠ ∅ )
4		df-cur	⊢ curry 𝐹 = ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } )
5	1	dmmpoga	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 → dom 𝐹 = ( 𝑋 × 𝑌 ) )
6	2 5	syl	⊢ ( 𝜑 → dom 𝐹 = ( 𝑋 × 𝑌 ) )
7	6	dmeqd	⊢ ( 𝜑 → dom dom 𝐹 = dom ( 𝑋 × 𝑌 ) )
8		dmxp	⊢ ( 𝑌 ≠ ∅ → dom ( 𝑋 × 𝑌 ) = 𝑋 )
9	3 8	syl	⊢ ( 𝜑 → dom ( 𝑋 × 𝑌 ) = 𝑋 )
10	7 9	eqtrd	⊢ ( 𝜑 → dom dom 𝐹 = 𝑋 )
11	10	mpteq1d	⊢ ( 𝜑 → ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝑋 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) )
12		df-mpt	⊢ ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝐶 ) }
13	1	mpofun	⊢ Fun 𝐹
14		funbrfv2b	⊢ ( Fun 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
15	13 14	mp1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
16	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → dom 𝐹 = ( 𝑋 × 𝑌 ) )
17	16	eleq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) ) )
18		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) )
19	17 18	bitrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) )
20	19	anbi1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
21		an21	⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( 𝑦 ∈ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
22		ibar	⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
23	22	bicomd	⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) )
24	23	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) )
26		df-ov	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
27		nfcv	⊢ Ⅎ 𝑎 𝐶
28		nfcv	⊢ Ⅎ 𝑏 𝐶
29		nfcv	⊢ Ⅎ 𝑥 𝑏
30		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶
31	29 30	nfcsbw	⊢ Ⅎ 𝑥 ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
32		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
33		csbeq1a	⊢ ( 𝑥 = 𝑎 → 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
34		csbeq1a	⊢ ( 𝑦 = 𝑏 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
35	33 34	sylan9eq	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝐶 = ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
36	27 28 31 32 35	cbvmpo	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) = ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑌 ↦ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
37	1 36	eqtri	⊢ 𝐹 = ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑌 ↦ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
38	37	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐹 = ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑌 ↦ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) )
39	33	eqcomd	⊢ ( 𝑥 = 𝑎 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = 𝐶 )
40	39	equcoms	⊢ ( 𝑎 = 𝑥 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = 𝐶 )
41	40	csbeq2dv	⊢ ( 𝑎 = 𝑥 → ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑦 ⦌ 𝐶 )
42		csbeq1a	⊢ ( 𝑦 = 𝑏 → 𝐶 = ⦋ 𝑏 / 𝑦 ⦌ 𝐶 )
43	42	eqcomd	⊢ ( 𝑦 = 𝑏 → ⦋ 𝑏 / 𝑦 ⦌ 𝐶 = 𝐶 )
44	43	equcoms	⊢ ( 𝑏 = 𝑦 → ⦋ 𝑏 / 𝑦 ⦌ 𝐶 = 𝐶 )
45	41 44	sylan9eq	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = 𝐶 )
46	45	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) ) → ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = 𝐶 )
47		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
48	47	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
49		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
50		rsp2	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐶 ∈ 𝑉 ) )
51	2 50	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐶 ∈ 𝑉 ) )
52	51	impl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐶 ∈ 𝑉 )
53	38 46 48 49 52	ovmpod	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )
54	26 53	eqtr3id	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐶 )
55	54	eqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ 𝐶 = 𝑧 ) )
56		eqcom	⊢ ( 𝐶 = 𝑧 ↔ 𝑧 = 𝐶 )
57	55 56	bitrdi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ 𝑧 = 𝐶 ) )
58	25 57	bitrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ 𝑧 = 𝐶 ) )
59	58	pm5.32da	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) ↔ ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝐶 ) ) )
60	21 59	syl5bb	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝐶 ) ) )
61	15 20 60	3bitrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝐶 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ) )
62	61	opabbidv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝐶 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } )
63	12 62	eqtr2id	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } = ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) )
64	63	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) )
65	11 64	eqtrd	⊢ ( 𝜑 → ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) )
66	4 65	eqtrid	⊢ ( 𝜑 → curry 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) )