mpt3fvd

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

	Ref	Expression
Hypotheses	mpt3fvd.1	$⊢ φ \to X \in ((A \times B) \times C)$
	mpt3fvd.2	$⊢ φ \to Y \in V$
	mpt3fvd.3	$⊢ (φ \land X = ⟨x, y, z⟩) \to Y = D$
	mpt3fvd.4	$⊢ F = (x \in A, y \in B, z \in C ⟼ D)$
Assertion	mpt3fvd	$⊢ φ \to F (X) = Y$

Proof

Step	Hyp	Ref	Expression
1		mpt3fvd.1	$⊢ φ \to X \in ((A \times B) \times C)$
2		mpt3fvd.2	$⊢ φ \to Y \in V$
3		mpt3fvd.3	$⊢ (φ \land X = ⟨x, y, z⟩) \to Y = D$
4		mpt3fvd.4	$⊢ F = (x \in A, y \in B, z \in C ⟼ D)$
5		el2xptp	$⊢ X \in ((A \times B) \times C) \leftrightarrow \exists x \in A \exists y \in B \exists z \in C X = ⟨x, y, z⟩$
6	1 5	sylib	$⊢ φ \to \exists x \in A \exists y \in B \exists z \in C X = ⟨x, y, z⟩$
7		simpr	$⊢ (φ \land X = ⟨x, y, z⟩) \to X = ⟨x, y, z⟩$
8	7 3	jca	$⊢ (φ \land X = ⟨x, y, z⟩) \to (X = ⟨x, y, z⟩ \land Y = D)$
9	8	ex	$⊢ φ \to (X = ⟨x, y, z⟩ \to (X = ⟨x, y, z⟩ \land Y = D))$
10	9	reximdv	$⊢ φ \to (\exists z \in C X = ⟨x, y, z⟩ \to \exists z \in C (X = ⟨x, y, z⟩ \land Y = D))$
11	10	reximdv	$⊢ φ \to (\exists y \in B \exists z \in C X = ⟨x, y, z⟩ \to \exists y \in B \exists z \in C (X = ⟨x, y, z⟩ \land Y = D))$
12	11	reximdv	$⊢ φ \to (\exists x \in A \exists y \in B \exists z \in C X = ⟨x, y, z⟩ \to \exists x \in A \exists y \in B \exists z \in C (X = ⟨x, y, z⟩ \land Y = D))$
13	6 12	mpd	$⊢ φ \to \exists x \in A \exists y \in B \exists z \in C (X = ⟨x, y, z⟩ \land Y = D)$
14	1	elexd	$⊢ φ \to X \in V$
15		eqeq1	$⊢ v = X \to (v = ⟨x, y, z⟩ \leftrightarrow X = ⟨x, y, z⟩)$
16	15	anbi1d	$⊢ v = X \to ((v = ⟨x, y, z⟩ \land w = D) \leftrightarrow (X = ⟨x, y, z⟩ \land w = D))$
17	16	rexbidv	$⊢ v = X \to (\exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists z \in C (X = ⟨x, y, z⟩ \land w = D))$
18	17	2rexbidv	$⊢ v = X \to (\exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists x \in A \exists y \in B \exists z \in C (X = ⟨x, y, z⟩ \land w = D))$
19		eqeq1	$⊢ w = Y \to (w = D \leftrightarrow Y = D)$
20	19	anbi2d	$⊢ w = Y \to ((X = ⟨x, y, z⟩ \land w = D) \leftrightarrow (X = ⟨x, y, z⟩ \land Y = D))$
21	20	rexbidv	$⊢ w = Y \to (\exists z \in C (X = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists z \in C (X = ⟨x, y, z⟩ \land Y = D))$
22	21	2rexbidv	$⊢ w = Y \to (\exists x \in A \exists y \in B \exists z \in C (X = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists x \in A \exists y \in B \exists z \in C (X = ⟨x, y, z⟩ \land Y = D))$
23		moeq	$⊢ \exists^{*} w w = D$
24	23	moani	$⊢ \exists^{*} w ((x \in A \land y \in B \land z \in C) \land w = D)$
25	24	ax-gen	$⊢ \forall z \exists^{*} w ((x \in A \land y \in B \land z \in C) \land w = D)$
26	25	gen2	$⊢ \forall x \forall y \forall z \exists^{*} w ((x \in A \land y \in B \land z \in C) \land w = D)$
27		mosubott	$⊢ \forall x \forall y \forall z \exists^{} w ((x \in A \land y \in B \land z \in C) \land w = D) \to \exists^{} w \exists x \exists y \exists z (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D))$
28	26 27	ax-mp	$⊢ \exists^{*} w \exists x \exists y \exists z (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D))$
29		r3ex	$⊢ \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists x \exists y \exists z ((x \in A \land y \in B \land z \in C) \land (v = ⟨x, y, z⟩ \land w = D))$
30		an12	$⊢ (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D)) \leftrightarrow ((x \in A \land y \in B \land z \in C) \land (v = ⟨x, y, z⟩ \land w = D))$
31	30	3exbii	$⊢ \exists x \exists y \exists z (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D)) \leftrightarrow \exists x \exists y \exists z ((x \in A \land y \in B \land z \in C) \land (v = ⟨x, y, z⟩ \land w = D))$
32	29 31	bitr4i	$⊢ \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists x \exists y \exists z (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D))$
33	32	mobii	$⊢ \exists^{} w \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists^{} w \exists x \exists y \exists z (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D))$
34	28 33	mpbir	$⊢ \exists^{*} w \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)$
35	34	a1i	$⊢ v \in V \to \exists^{*} w \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)$
36		df-mpt3	$⊢ (x \in A, y \in B, z \in C ⟼ D) = \{⟨v, w⟩ \| \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)\}$
37		vex	$⊢ v \in V$
38	37	biantrur	$⊢ \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow (v \in V \land \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D))$
39	38	opabbii	$⊢ \{⟨v, w⟩ \| \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)\} = \{⟨v, w⟩ \| (v \in V \land \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D))\}$
40	36 39	eqtri	$⊢ (x \in A, y \in B, z \in C ⟼ D) = \{⟨v, w⟩ \| (v \in V \land \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D))\}$
41	18 22 35 40	fvopab3ig	$⊢ (X \in V \land Y \in V) \to (\exists x \in A \exists y \in B \exists z \in C (X = ⟨x, y, z⟩ \land Y = D) \to (x \in A, y \in B, z \in C ⟼ D) (X) = Y)$
42	4	fveq1i	$⊢ F (X) = (x \in A, y \in B, z \in C ⟼ D) (X)$
43	42	eqeq1i	$⊢ F (X) = Y \leftrightarrow (x \in A, y \in B, z \in C ⟼ D) (X) = Y$
44	41 43	imbitrrdi	$⊢ (X \in V \land Y \in V) \to (\exists x \in A \exists y \in B \exists z \in C (X = ⟨x, y, z⟩ \land Y = D) \to F (X) = Y)$
45	14 2 44	syl2anc	$⊢ φ \to (\exists x \in A \exists y \in B \exists z \in C (X = ⟨x, y, z⟩ \land Y = D) \to F (X) = Y)$
46	13 45	mpd	$⊢ φ \to F (X) = Y$

Metamath Proof Explorer

Theorem mpt3fvd

Proof