Theorem funmpt3

Description: A function in maps-to notation with three arguments is a function. (Contributed by BTernaryTau, 8-Sep-2026)

	Ref	Expression
Assertion	funmpt3	⊢ Fun ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		funopab	⊢ ( Fun { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) } ↔ ∀ 𝑣 ∃* 𝑤 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) )
2		moeq	⊢ ∃* 𝑤 𝑤 = 𝐷
3	2	moani	⊢ ∃* 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 )
4	3	ax-gen	⊢ ∀ 𝑧 ∃* 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 )
5	4	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∃* 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 )
6		mosubott	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∃* 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) → ∃* 𝑤 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) ) )
7	5 6	ax-mp	⊢ ∃* 𝑤 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) )
8		r3ex	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) )
9		an12	⊢ ( ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) )
10	9	3exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ) )
11	8 10	bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) ) )
12	11	mobii	⊢ ( ∃* 𝑤 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) ↔ ∃* 𝑤 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑤 = 𝐷 ) ) )
13	7 12	mpbir	⊢ ∃* 𝑤 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 )
14	1 13	mpgbir	⊢ Fun { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) }
15		df-mpt3	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) }
16	15	funeqi	⊢ ( Fun ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) ↔ Fun { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑣 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑤 = 𝐷 ) } )
17	14 16	mpbir	⊢ Fun ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 )