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	|- ( ph -> R e. A )
	mpofvop2d.2	|- ( ph -> S e. B )
	mpofvop2d.3	|- ( ph -> L e. V )
	mpofvop2d.4	|- ( ( ph /\ R = x ) -> K = C )
	mpofvop2d.5	|- ( ( ph /\ S = y ) -> L = K )
	mpofvop2d.6	|- F = ( x e. A , y e. B |-> C )
Assertion	mpofvop2d	|- ( ph -> ( F ` <. R , S >. ) = L )

Proof

Step	Hyp	Ref	Expression
1		mpofvop2d.1	|- ( ph -> R e. A )
2		mpofvop2d.2	|- ( ph -> S e. B )
3		mpofvop2d.3	|- ( ph -> L e. V )
4		mpofvop2d.4	|- ( ( ph /\ R = x ) -> K = C )
5		mpofvop2d.5	|- ( ( ph /\ S = y ) -> L = K )
6		mpofvop2d.6	|- F = ( x e. A , y e. B |-> C )
7		opthg	|- ( ( R e. A /\ S e. B ) -> ( <. R , S >. = <. x , y >. <-> ( R = x /\ S = y ) ) )
8	1 2 7	syl2anc	|- ( ph -> ( <. R , S >. = <. x , y >. <-> ( R = x /\ S = y ) ) )
9	4	ex	|- ( ph -> ( R = x -> K = C ) )
10	5	ex	|- ( ph -> ( S = y -> L = K ) )
11	9 10	anim12d	|- ( ph -> ( ( R = x /\ S = y ) -> ( K = C /\ L = K ) ) )
12	8 11	sylbid	|- ( ph -> ( <. R , S >. = <. x , y >. -> ( K = C /\ L = K ) ) )
13		eqtr	|- ( ( L = K /\ K = C ) -> L = C )
14	13	ancoms	|- ( ( K = C /\ L = K ) -> L = C )
15	12 14	syl6	|- ( ph -> ( <. R , S >. = <. x , y >. -> L = C ) )
16	15	imp	|- ( ( ph /\ <. R , S >. = <. x , y >. ) -> L = C )
17	1 2 3 16 6	mpofvopd	|- ( ph -> ( F ` <. R , S >. ) = L )