Metamath Proof Explorer


Theorem uncov

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

Ref Expression
Assertion uncov ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴 uncurry 𝐹 𝐵 ) = ( ( 𝐹𝐴 ) ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-br ( ⟨ 𝐴 , 𝐵 ⟩ uncurry 𝐹 𝑤 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑤 ⟩ ∈ uncurry 𝐹 )
2 df-unc uncurry 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐹𝑥 ) 𝑧 }
3 2 eleq2i ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑤 ⟩ ∈ uncurry 𝐹 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐹𝑥 ) 𝑧 } )
4 1 3 bitri ( ⟨ 𝐴 , 𝐵 ⟩ uncurry 𝐹 𝑤 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐹𝑥 ) 𝑧 } )
5 vex 𝑤 ∈ V
6 simp2 ( ( 𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝑤 ) → 𝑦 = 𝐵 )
7 fveq2 ( 𝑥 = 𝐴 → ( 𝐹𝑥 ) = ( 𝐹𝐴 ) )
8 7 3ad2ant1 ( ( 𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝑤 ) → ( 𝐹𝑥 ) = ( 𝐹𝐴 ) )
9 simp3 ( ( 𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝑤 ) → 𝑧 = 𝑤 )
10 6 8 9 breq123d ( ( 𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝑤 ) → ( 𝑦 ( 𝐹𝑥 ) 𝑧𝐵 ( 𝐹𝐴 ) 𝑤 ) )
11 10 eloprabga ( ( 𝐴𝑉𝐵𝑊𝑤 ∈ V ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐹𝑥 ) 𝑧 } ↔ 𝐵 ( 𝐹𝐴 ) 𝑤 ) )
12 5 11 mp3an3 ( ( 𝐴𝑉𝐵𝑊 ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐹𝑥 ) 𝑧 } ↔ 𝐵 ( 𝐹𝐴 ) 𝑤 ) )
13 4 12 syl5bb ( ( 𝐴𝑉𝐵𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ uncurry 𝐹 𝑤𝐵 ( 𝐹𝐴 ) 𝑤 ) )
14 13 iotabidv ( ( 𝐴𝑉𝐵𝑊 ) → ( ℩ 𝑤𝐴 , 𝐵 ⟩ uncurry 𝐹 𝑤 ) = ( ℩ 𝑤 𝐵 ( 𝐹𝐴 ) 𝑤 ) )
15 df-ov ( 𝐴 uncurry 𝐹 𝐵 ) = ( uncurry 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
16 df-fv ( uncurry 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ℩ 𝑤𝐴 , 𝐵 ⟩ uncurry 𝐹 𝑤 )
17 15 16 eqtri ( 𝐴 uncurry 𝐹 𝐵 ) = ( ℩ 𝑤𝐴 , 𝐵 ⟩ uncurry 𝐹 𝑤 )
18 df-fv ( ( 𝐹𝐴 ) ‘ 𝐵 ) = ( ℩ 𝑤 𝐵 ( 𝐹𝐴 ) 𝑤 )
19 14 17 18 3eqtr4g ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴 uncurry 𝐹 𝐵 ) = ( ( 𝐹𝐴 ) ‘ 𝐵 ) )