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	$$⊢\phi \to R\in A$$
	mpt3fvot2d.2	$$⊢\phi \to S\in B$$
	mpt3fvot2d.3	$$⊢\phi \to T\in C$$
	mpt3fvot2d.4	$$⊢\phi \to M\in V$$
	mpt3fvot2d.5	$$⊢\left(\phi \wedge R=x\right)\to K=D$$
	mpt3fvot2d.6	$$⊢\left(\phi \wedge S=y\right)\to L=K$$
	mpt3fvot2d.7	$$⊢\left(\phi \wedge T=z\right)\to M=L$$
	mpt3fvot2d.8	$$⊢F=\left(x\in A,y\in B,z\in C⟼D\right)$$
Assertion	mpt3fvot2d	$$⊢\phi \to F\left(⟨R,S,T⟩\right)=M$$

Proof

Step	Hyp	Ref	Expression
1		mpt3fvot2d.1	$$⊢\phi \to R\in A$$
2		mpt3fvot2d.2	$$⊢\phi \to S\in B$$
3		mpt3fvot2d.3	$$⊢\phi \to T\in C$$
4		mpt3fvot2d.4	$$⊢\phi \to M\in V$$
5		mpt3fvot2d.5	$$⊢\left(\phi \wedge R=x\right)\to K=D$$
6		mpt3fvot2d.6	$$⊢\left(\phi \wedge S=y\right)\to L=K$$
7		mpt3fvot2d.7	$$⊢\left(\phi \wedge T=z\right)\to M=L$$
8		mpt3fvot2d.8	$$⊢F=\left(x\in A,y\in B,z\in C⟼D\right)$$
9		otthg	$$⊢\left(R\in A\wedge S\in B\wedge T\in C\right)\to \left(⟨R,S,T⟩=⟨x,y,z⟩\leftrightarrow \left(R=x\wedge S=y\wedge T=z\right)\right)$$
10	1 2 3 9	syl3anc	$$⊢\phi \to \left(⟨R,S,T⟩=⟨x,y,z⟩\leftrightarrow \left(R=x\wedge S=y\wedge T=z\right)\right)$$
11	5	ex	$$⊢\phi \to \left(R=x\to K=D\right)$$
12	6	ex	$$⊢\phi \to \left(S=y\to L=K\right)$$
13	7	ex	$$⊢\phi \to \left(T=z\to M=L\right)$$
14	11 12 13	3anim123d	$$⊢\phi \to \left(\left(R=x\wedge S=y\wedge T=z\right)\to \left(K=D\wedge L=K\wedge M=L\right)\right)$$
15	10 14	sylbid	$$⊢\phi \to \left(⟨R,S,T⟩=⟨x,y,z⟩\to \left(K=D\wedge L=K\wedge M=L\right)\right)$$
16		eqtr	$$⊢\left(L=K\wedge K=D\right)\to L=D$$
17		eqtr	$$⊢\left(M=L\wedge L=D\right)\to M=D$$
18	17	ancoms	$$⊢\left(L=D\wedge M=L\right)\to M=D$$
19	16 18	sylan	$$⊢\left(\left(L=K\wedge K=D\right)\wedge M=L\right)\to M=D$$
20	19	ancom1s	$$⊢\left(\left(K=D\wedge L=K\right)\wedge M=L\right)\to M=D$$
21	20	3impa	$$⊢\left(K=D\wedge L=K\wedge M=L\right)\to M=D$$
22	15 21	syl6	$$⊢\phi \to \left(⟨R,S,T⟩=⟨x,y,z⟩\to M=D\right)$$
23	22	imp	$$⊢\left(\phi \wedge ⟨R,S,T⟩=⟨x,y,z⟩\right)\to M=D$$
24	1 2 3 4 23 8	mpt3fvotd	$$⊢\phi \to F\left(⟨R,S,T⟩\right)=M$$