Theorem uncf

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

	Ref	Expression
Assertion	uncf	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → uncurry 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		ffvelcdm	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐶 ↑m 𝐵 ) )
2		elmapi	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐶 ↑m 𝐵 ) → ( 𝐹 ‘ 𝑥 ) : 𝐵 ⟶ 𝐶 )
3	1 2	syl	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) : 𝐵 ⟶ 𝐶 )
4	3	ffvelcdmda	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ∈ 𝐶 )
5	4	anasss	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ∈ 𝐶 )
6	5	ralrimivva	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ∈ 𝐶 )
7		df-unc	⊢ uncurry 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 }
8		df-br	⊢ ( 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐹 ‘ 𝑥 ) )
9		elfvdm	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐹 ‘ 𝑥 ) → 𝑥 ∈ dom 𝐹 )
10	8 9	sylbi	⊢ ( 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 → 𝑥 ∈ dom 𝐹 )
11		fdm	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → dom 𝐹 = 𝐴 )
12	11	eleq2d	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴 ) )
13	10 12	imbitrid	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 → 𝑥 ∈ 𝐴 ) )
14	13	pm4.71rd	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 ) ) )
15		elmapfun	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐶 ↑m 𝐵 ) → Fun ( 𝐹 ‘ 𝑥 ) )
16		funbrfv2b	⊢ ( Fun ( 𝐹 ‘ 𝑥 ) → ( 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 ↔ ( 𝑦 ∈ dom ( 𝐹 ‘ 𝑥 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ) ) )
17	1 15 16	3syl	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 ↔ ( 𝑦 ∈ dom ( 𝐹 ‘ 𝑥 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ) ) )
18		fdm	⊢ ( ( 𝐹 ‘ 𝑥 ) : 𝐵 ⟶ 𝐶 → dom ( 𝐹 ‘ 𝑥 ) = 𝐵 )
19	1 2 18	3syl	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → dom ( 𝐹 ‘ 𝑥 ) = 𝐵 )
20	19	eleq2d	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ dom ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ 𝐵 ) )
21		eqcom	⊢ ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ↔ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) )
22	21	a1i	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ↔ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) )
23	20 22	anbi12d	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∈ dom ( 𝐹 ‘ 𝑥 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
24	17 23	bitrd	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
25	24	pm5.32da	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) )
26	14 25	bitrd	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) )
27		anass	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
28	26 27	bitr4di	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
29	28	oprabbidv	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) } )
30	7 29	eqtrid	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → uncurry 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) } )
31	30	feq1d	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( uncurry 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ↔ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) } : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ) )
32		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) }
33	32	eqcomi	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) } = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) )
34	33	fmpo	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ∈ 𝐶 ↔ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ) } : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
35	31 34	bitr4di	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( uncurry 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) ∈ 𝐶 ) )
36	6 35	mpbird	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → uncurry 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )