Theorem mpt3fvot2d

Description: Value of a three-argument function in maps-to notation at an ordered triple. (Contributed by BTernaryTau, 28-Sep-2026)

	Ref	Expression
Hypotheses	mpt3fvot2d.1	|- ( ph -> R e. A )
	mpt3fvot2d.2	|- ( ph -> S e. B )
	mpt3fvot2d.3	|- ( ph -> T e. C )
	mpt3fvot2d.4	|- ( ph -> M e. V )
	mpt3fvot2d.5	|- ( ( ph /\ R = x ) -> K = D )
	mpt3fvot2d.6	|- ( ( ph /\ S = y ) -> L = K )
	mpt3fvot2d.7	|- ( ( ph /\ T = z ) -> M = L )
	mpt3fvot2d.8	|- F = ( x e. A , y e. B , z e. C |-> D )
Assertion	mpt3fvot2d	|- ( ph -> ( F ` <. R , S , T >. ) = M )

Proof

Step	Hyp	Ref	Expression
1		mpt3fvot2d.1	|- ( ph -> R e. A )
2		mpt3fvot2d.2	|- ( ph -> S e. B )
3		mpt3fvot2d.3	|- ( ph -> T e. C )
4		mpt3fvot2d.4	|- ( ph -> M e. V )
5		mpt3fvot2d.5	|- ( ( ph /\ R = x ) -> K = D )
6		mpt3fvot2d.6	|- ( ( ph /\ S = y ) -> L = K )
7		mpt3fvot2d.7	|- ( ( ph /\ T = z ) -> M = L )
8		mpt3fvot2d.8	|- F = ( x e. A , y e. B , z e. C |-> D )
9		otthg	|- ( ( R e. A /\ S e. B /\ T e. C ) -> ( <. R , S , T >. = <. x , y , z >. <-> ( R = x /\ S = y /\ T = z ) ) )
10	1 2 3 9	syl3anc	|- ( ph -> ( <. R , S , T >. = <. x , y , z >. <-> ( R = x /\ S = y /\ T = z ) ) )
11	5	ex	|- ( ph -> ( R = x -> K = D ) )
12	6	ex	|- ( ph -> ( S = y -> L = K ) )
13	7	ex	|- ( ph -> ( T = z -> M = L ) )
14	11 12 13	3anim123d	|- ( ph -> ( ( R = x /\ S = y /\ T = z ) -> ( K = D /\ L = K /\ M = L ) ) )
15	10 14	sylbid	|- ( ph -> ( <. R , S , T >. = <. x , y , z >. -> ( K = D /\ L = K /\ M = L ) ) )
16		eqtr	|- ( ( L = K /\ K = D ) -> L = D )
17		eqtr	|- ( ( M = L /\ L = D ) -> M = D )
18	17	ancoms	|- ( ( L = D /\ M = L ) -> M = D )
19	16 18	sylan	|- ( ( ( L = K /\ K = D ) /\ M = L ) -> M = D )
20	19	ancom1s	|- ( ( ( K = D /\ L = K ) /\ M = L ) -> M = D )
21	20	3impa	|- ( ( K = D /\ L = K /\ M = L ) -> M = D )
22	15 21	syl6	|- ( ph -> ( <. R , S , T >. = <. x , y , z >. -> M = D ) )
23	22	imp	|- ( ( ph /\ <. R , S , T >. = <. x , y , z >. ) -> M = D )
24	1 2 3 4 23 8	mpt3fvotd	|- ( ph -> ( F ` <. R , S , T >. ) = M )