Theorem mpofvop2d

Description: Value of a two-argument function (usually an operation) in maps-to notation at an ordered pair. (Contributed by BTernaryTau, 18-Oct-2026)

	Ref	Expression
Hypotheses	mpofvop2d.1	$$⊢\phi \to R\in A$$
	mpofvop2d.2	$$⊢\phi \to S\in B$$
	mpofvop2d.3	$$⊢\phi \to L\in V$$
	mpofvop2d.4	$$⊢\left(\phi \wedge R=x\right)\to K=C$$
	mpofvop2d.5	$$⊢\left(\phi \wedge S=y\right)\to L=K$$
	mpofvop2d.6	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
Assertion	mpofvop2d	$$⊢\phi \to F\left(⟨R,S⟩\right)=L$$

Proof

Step	Hyp	Ref	Expression
1		mpofvop2d.1	$$⊢\phi \to R\in A$$
2		mpofvop2d.2	$$⊢\phi \to S\in B$$
3		mpofvop2d.3	$$⊢\phi \to L\in V$$
4		mpofvop2d.4	$$⊢\left(\phi \wedge R=x\right)\to K=C$$
5		mpofvop2d.5	$$⊢\left(\phi \wedge S=y\right)\to L=K$$
6		mpofvop2d.6	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
7		opthg	$$⊢\left(R\in A\wedge S\in B\right)\to \left(⟨R,S⟩=⟨x,y⟩\leftrightarrow \left(R=x\wedge S=y\right)\right)$$
8	1 2 7	syl2anc	$$⊢\phi \to \left(⟨R,S⟩=⟨x,y⟩\leftrightarrow \left(R=x\wedge S=y\right)\right)$$
9	4	ex	$$⊢\phi \to \left(R=x\to K=C\right)$$
10	5	ex	$$⊢\phi \to \left(S=y\to L=K\right)$$
11	9 10	anim12d	$$⊢\phi \to \left(\left(R=x\wedge S=y\right)\to \left(K=C\wedge L=K\right)\right)$$
12	8 11	sylbid	$$⊢\phi \to \left(⟨R,S⟩=⟨x,y⟩\to \left(K=C\wedge L=K\right)\right)$$
13		eqtr	$$⊢\left(L=K\wedge K=C\right)\to L=C$$
14	13	ancoms	$$⊢\left(K=C\wedge L=K\right)\to L=C$$
15	12 14	syl6	$$⊢\phi \to \left(⟨R,S⟩=⟨x,y⟩\to L=C\right)$$
16	15	imp	$$⊢\left(\phi \wedge ⟨R,S⟩=⟨x,y⟩\right)\to L=C$$
17	1 2 3 16 6	mpofvopd	$$⊢\phi \to F\left(⟨R,S⟩\right)=L$$