Metamath Proof Explorer


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 ffvelrn ( ( 𝐹 : 𝐴 ⟶ ( 𝐶m 𝐵 ) ∧ 𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ( 𝐶m 𝐵 ) )
2 elmapi ( ( 𝐹𝑥 ) ∈ ( 𝐶m 𝐵 ) → ( 𝐹𝑥 ) : 𝐵𝐶 )
3 1 2 syl ( ( 𝐹 : 𝐴 ⟶ ( 𝐶m 𝐵 ) ∧ 𝑥𝐴 ) → ( 𝐹𝑥 ) : 𝐵𝐶 )
4 3 ffvelrnda ( ( ( 𝐹 : 𝐴 ⟶ ( 𝐶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 syl5ib ( 𝐹 : 𝐴 ⟶ ( 𝐶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 syl5eq ( 𝐹 : 𝐴 ⟶ ( 𝐶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 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )