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	bitrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 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 𝐹 𝐵 ) = ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) )