Metamath Proof Explorer

Theorem uncov

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

Ref Expression
Assertion uncov ⊢ A ∈ V ∧ B ∈ W → A uncurry F B = F ⁡ A ⁡ B

Proof

Step Hyp Ref Expression
1 df-br ⊢ A B uncurry F w ↔ A B w ∈ uncurry F
2 df-unc ⊢ uncurry F = x y z | y F ⁡ x z
3 2 eleq2i ⊢ A B w ∈ uncurry F ↔ A B w ∈ x y z | y F ⁡ x z
4 1 3 bitri ⊢ A B uncurry F w ↔ A B w ∈ x y z | y F ⁡ x z
5 vex ⊢ w ∈ V
6 simp2 ⊢ x = A ∧ y = B ∧ z = w → y = B
7 fveq2 ⊢ x = A → F ⁡ x = F ⁡ A
8 7 3ad2ant1 ⊢ x = A ∧ y = B ∧ z = w → F ⁡ x = F ⁡ A
9 simp3 ⊢ x = A ∧ y = B ∧ z = w → z = w
10 6 8 9 breq123d ⊢ x = A ∧ y = B ∧ z = w → y F ⁡ x z ↔ B F ⁡ A w
11 10 eloprabga ⊢ A ∈ V ∧ B ∈ W ∧ w ∈ V → A B w ∈ x y z | y F ⁡ x z ↔ B F ⁡ A w
12 5 11 mp3an3 ⊢ A ∈ V ∧ B ∈ W → A B w ∈ x y z | y F ⁡ x z ↔ B F ⁡ A w
13 4 12 bitrid ⊢ A ∈ V ∧ B ∈ W → A B uncurry F w ↔ B F ⁡ A w
14 13 iotabidv ⊢ A ∈ V ∧ B ∈ W → ι w | A B uncurry F w = ι w | B F ⁡ A w
15 df-ov ⊢ A uncurry F B = uncurry F ⁡ A B
16 df-fv ⊢ uncurry F ⁡ A B = ι w | A B uncurry F w
17 15 16 eqtri ⊢ A uncurry F B = ι w | A B uncurry F w
18 df-fv ⊢ F ⁡ A ⁡ B = ι w | B F ⁡ A w
19 14 17 18 3eqtr4g ⊢ A ∈ V ∧ B ∈ W → A uncurry F B = F ⁡ A ⁡ B