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 𝐹 𝐵 ) = ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) ) |