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	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
	mpt3fvot2d.2	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
	mpt3fvot2d.3	⊢ ( 𝜑 → 𝑇 ∈ 𝐶 )
	mpt3fvot2d.4	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
	mpt3fvot2d.5	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑥 ) → 𝐾 = 𝐷 )
	mpt3fvot2d.6	⊢ ( ( 𝜑 ∧ 𝑆 = 𝑦 ) → 𝐿 = 𝐾 )
	mpt3fvot2d.7	⊢ ( ( 𝜑 ∧ 𝑇 = 𝑧 ) → 𝑀 = 𝐿 )
	mpt3fvot2d.8	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 )
Assertion	mpt3fvot2d	⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ ) = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		mpt3fvot2d.1	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
2		mpt3fvot2d.2	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
3		mpt3fvot2d.3	⊢ ( 𝜑 → 𝑇 ∈ 𝐶 )
4		mpt3fvot2d.4	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
5		mpt3fvot2d.5	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑥 ) → 𝐾 = 𝐷 )
6		mpt3fvot2d.6	⊢ ( ( 𝜑 ∧ 𝑆 = 𝑦 ) → 𝐿 = 𝐾 )
7		mpt3fvot2d.7	⊢ ( ( 𝜑 ∧ 𝑇 = 𝑧 ) → 𝑀 = 𝐿 )
8		mpt3fvot2d.8	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 )
9		otthg	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐶 ) → ( ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ↔ ( 𝑅 = 𝑥 ∧ 𝑆 = 𝑦 ∧ 𝑇 = 𝑧 ) ) )
10	1 2 3 9	syl3anc	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ↔ ( 𝑅 = 𝑥 ∧ 𝑆 = 𝑦 ∧ 𝑇 = 𝑧 ) ) )
11	5	ex	⊢ ( 𝜑 → ( 𝑅 = 𝑥 → 𝐾 = 𝐷 ) )
12	6	ex	⊢ ( 𝜑 → ( 𝑆 = 𝑦 → 𝐿 = 𝐾 ) )
13	7	ex	⊢ ( 𝜑 → ( 𝑇 = 𝑧 → 𝑀 = 𝐿 ) )
14	11 12 13	3anim123d	⊢ ( 𝜑 → ( ( 𝑅 = 𝑥 ∧ 𝑆 = 𝑦 ∧ 𝑇 = 𝑧 ) → ( 𝐾 = 𝐷 ∧ 𝐿 = 𝐾 ∧ 𝑀 = 𝐿 ) ) )
15	10 14	sylbid	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝐾 = 𝐷 ∧ 𝐿 = 𝐾 ∧ 𝑀 = 𝐿 ) ) )
16		eqtr	⊢ ( ( 𝐿 = 𝐾 ∧ 𝐾 = 𝐷 ) → 𝐿 = 𝐷 )
17		eqtr	⊢ ( ( 𝑀 = 𝐿 ∧ 𝐿 = 𝐷 ) → 𝑀 = 𝐷 )
18	17	ancoms	⊢ ( ( 𝐿 = 𝐷 ∧ 𝑀 = 𝐿 ) → 𝑀 = 𝐷 )
19	16 18	sylan	⊢ ( ( ( 𝐿 = 𝐾 ∧ 𝐾 = 𝐷 ) ∧ 𝑀 = 𝐿 ) → 𝑀 = 𝐷 )
20	19	ancom1s	⊢ ( ( ( 𝐾 = 𝐷 ∧ 𝐿 = 𝐾 ) ∧ 𝑀 = 𝐿 ) → 𝑀 = 𝐷 )
21	20	3impa	⊢ ( ( 𝐾 = 𝐷 ∧ 𝐿 = 𝐾 ∧ 𝑀 = 𝐿 ) → 𝑀 = 𝐷 )
22	15 21	syl6	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → 𝑀 = 𝐷 ) )
23	22	imp	⊢ ( ( 𝜑 ∧ ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝑀 = 𝐷 )
24	1 2 3 4 23 8	mpt3fvotd	⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ ) = 𝑀 )