Metamath Proof Explorer

Theorem mpt3fvd

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

Ref Expression
Hypotheses mpt3fvd.1 ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
mpt3fvd.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
mpt3fvd.3 ⊢ ( ( 𝜑 ∧ 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝑌 = 𝐷 )
mpt3fvd.4 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 )
Assertion mpt3fvd ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 mpt3fvd.1 ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
2 mpt3fvd.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
3 mpt3fvd.3 ⊢ ( ( 𝜑 ∧ 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝑌 = 𝐷 )
4 mpt3fvd.4 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 )
5 el2xptp ⊢ ( 𝑋 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
6 1 5 sylib ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
8 7 3 jca ⊢ ( ( 𝜑 ∧ 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) )
9 8 ex ⊢ ( 𝜑 → ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) ) )
10 9 reximdv ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ 𝐶 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) ) )
11 10 reximdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) ) )
12 11 reximdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) ) )
13 6 12 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) )
14 1 elexd ⊢ ( 𝜑 → 𝑋 ∈ V )
15 eqeq1 ⊢ ( 𝑣 = 𝑋 → ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ↔ 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) )
16 15 anbi1d ⊢ ( 𝑣 = 𝑋 → ( ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) )
17 16 rexbidv ⊢ ( 𝑣 = 𝑋 → ( ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) )
18 17 2rexbidv ⊢ ( 𝑣 = 𝑋 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) )
19 eqeq1 ⊢ ( 𝑤 = 𝑌 → ( 𝑤 = 𝐷 ↔ 𝑌 = 𝐷 ) )
20 19 anbi2d ⊢ ( 𝑤 = 𝑌 → ( ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) ) )
21 20 rexbidv ⊢ ( 𝑤 = 𝑌 → ( ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) ) )
22 21 2rexbidv ⊢ ( 𝑤 = 𝑌 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) ) )
23 moeq ⊢ ∃* 𝑤 𝑤 = 𝐷
24 23 moani ⊢ ∃* 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 )
25 24 ax-gen ⊢ ∀ 𝑧 ∃* 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 )
26 25 gen2 ⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∃* 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 )
27 mosubott ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∃* 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) → ∃* 𝑤 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) ) )
28 26 27 ax-mp ⊢ ∃* 𝑤 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) )
29 r3ex ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) )
30 an12 ⊢ ( ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) )
31 30 3exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) )
32 29 31 bitr4i ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) ) )
33 32 mobii ⊢ ( ∃* 𝑤 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃* 𝑤 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) ) )
34 28 33 mpbir ⊢ ∃* 𝑤 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 )
35 34 a1i ⊢ ( 𝑣 ∈ V → ∃* 𝑤 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) )
36 df-mpt3 ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) }
37 vex ⊢ 𝑣 ∈ V
38 37 biantrur ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ( 𝑣 ∈ V ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) )
39 38 opabbii ⊢ { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) } = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣 ∈ V ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) }
40 36 39 eqtri ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ( 𝑣 ∈ V ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) }
41 18 22 35 40 fvopab3ig ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ 𝑉 ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) → ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑋 ) = 𝑌 ) )
42 4 fveq1i ⊢ ( 𝐹 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑋 )
43 42 eqeq1i ⊢ ( ( 𝐹 ‘ 𝑋 ) = 𝑌 ↔ ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑋 ) = 𝑌 )
44 41 43 imbitrrdi ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ 𝑉 ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) → ( 𝐹 ‘ 𝑋 ) = 𝑌 ) )
45 14 2 44 syl2anc ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑋 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑌 = 𝐷 ) → ( 𝐹 ‘ 𝑋 ) = 𝑌 ) )
46 13 45 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑌 )