Theorem curunc

Description: Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021)

	Ref	Expression
Assertion	curunc	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝐵 ≠ ∅ ) → curry uncurry 𝐹 = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝐵 ≠ ∅ ) → 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) )
2	1	feqmptd	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝐵 ≠ ∅ ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
3		uncf	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → uncurry 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
4	3	fdmd	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → dom uncurry 𝐹 = ( 𝐴 × 𝐵 ) )
5	4	dmeqd	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → dom dom uncurry 𝐹 = dom ( 𝐴 × 𝐵 ) )
6		dmxp	⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
7	5 6	sylan9eq	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝐵 ≠ ∅ ) → dom dom uncurry 𝐹 = 𝐴 )
8	7	eqcomd	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝐵 ≠ ∅ ) → 𝐴 = dom dom uncurry 𝐹 )
9		df-mpt	⊢ ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) }
10		ffvelcdm	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐶 ↑m 𝐵 ) )
11		elmapi	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐶 ↑m 𝐵 ) → ( 𝐹 ‘ 𝑥 ) : 𝐵 ⟶ 𝐶 )
12	10 11	syl	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) : 𝐵 ⟶ 𝐶 )
13	12	feqmptd	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) )
14		ffun	⊢ ( uncurry 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → Fun uncurry 𝐹 )
15		funbrfv2b	⊢ ( Fun uncurry 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ uncurry 𝐹 𝑧 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom uncurry 𝐹 ∧ ( uncurry 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
16	3 14 15	3syl	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ uncurry 𝐹 𝑧 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom uncurry 𝐹 ∧ ( uncurry 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
17	16	adantr	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ uncurry 𝐹 𝑧 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom uncurry 𝐹 ∧ ( uncurry 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
18	4	eleq2d	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom uncurry 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
19		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
20	19	baib	⊢ ( 𝑥 ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ 𝑦 ∈ 𝐵 ) )
21	18 20	sylan9bb	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom uncurry 𝐹 ↔ 𝑦 ∈ 𝐵 ) )
22		df-ov	⊢ ( 𝑥 uncurry 𝐹 𝑦 ) = ( uncurry 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
23		uncov	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 uncurry 𝐹 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) )
24	23	el2v	⊢ ( 𝑥 uncurry 𝐹 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 )
25	22 24	eqtr3i	⊢ ( uncurry 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 )
26	25	eqeq1i	⊢ ( ( uncurry 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 )
27		eqcom	⊢ ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ↔ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) )
28	26 27	bitri	⊢ ( ( uncurry 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) )
29	28	a1i	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( uncurry 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) )
30	21 29	anbi12d	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom uncurry 𝐹 ∧ ( uncurry 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
31	17 30	bitrd	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ uncurry 𝐹 𝑧 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
32	31	opabbidv	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ uncurry 𝐹 𝑧 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) } )
33	9 13 32	3eqtr4a	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ uncurry 𝐹 𝑧 } )
34	33	adantlr	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ uncurry 𝐹 𝑧 } )
35	8 34	mpteq12dva	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝐵 ≠ ∅ ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ dom dom uncurry 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ uncurry 𝐹 𝑧 } ) )
36		df-cur	⊢ curry uncurry 𝐹 = ( 𝑥 ∈ dom dom uncurry 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ uncurry 𝐹 𝑧 } )
37	35 36	eqtr4di	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝐵 ≠ ∅ ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = curry uncurry 𝐹 )
38	2 37	eqtr2d	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝐵 ≠ ∅ ) → curry uncurry 𝐹 = 𝐹 )