Theorem curf

Description: Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021)

	Ref	Expression
Assertion	curf	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
2		ffvelrn	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝐶 )
3	1 2	sylan2	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝐶 )
4	3	anassrs	⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝐶 )
5	4	fmpttd	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 )
6	5	3ad2antl1	⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 )
7		elmapg	⊢ ( ( 𝐶 ∈ 𝑊 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) → ( ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 ) )
8	7	ancoms	⊢ ( ( 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 ) )
9	8	3adant1	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 ) )
10	9	adantr	⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 ) )
11	6 10	mpbird	⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ ( 𝐶 ↑m 𝐵 ) )
12	11	fmpttd	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) )
13		eldifsni	⊢ ( 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) → 𝐵 ≠ ∅ )
14		df-cur	⊢ curry 𝐹 = ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } )
15		fdm	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → dom 𝐹 = ( 𝐴 × 𝐵 ) )
16	15	dmeqd	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → dom dom 𝐹 = dom ( 𝐴 × 𝐵 ) )
17		dmxp	⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
18	16 17	sylan9eq	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → dom dom 𝐹 = 𝐴 )
19	18	mpteq1d	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝐴 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) )
20		ffun	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → Fun 𝐹 )
21		funbrfv2b	⊢ ( Fun 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
22	20 21	syl	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
23	15	eleq2d	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
24		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
25	23 24	bitrdi	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
26	25	anbi1d	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
27	22 26	bitrd	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
28		ibar	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) )
29		anass	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
30		eqcom	⊢ ( 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 )
31	30	anbi2i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) )
32	29 31	bitr3i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) )
33	28 32	bitr2di	⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
34	27 33	sylan9bb	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
35	34	opabbidv	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) } )
36		df-mpt	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) }
37	35 36	eqtr4di	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } = ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
38	37	mpteq2dva	⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( 𝑥 ∈ 𝐴 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
39	38	adantr	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → ( 𝑥 ∈ 𝐴 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
40	19 39	eqtrd	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
41	14 40	syl5eq	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → curry 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
42	41	feq1d	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ) )
43	13 42	sylan2	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) → ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ) )
44	43	3adant3	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ) )
45	12 44	mpbird	⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) )