Definition df-bj-mpt3

Description: Define maps-to notation for functions with three arguments. See df-mpt and df-mpo for functions with one and two arguments respectively. This definition is analogous to bj-dfmpoa . (Contributed by BJ, 11-Apr-2020)

	Ref	Expression
Assertion	df-bj-mpt3	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑠 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		vy	⊢ 𝑦
3		cB	⊢ 𝐵
4		vz	⊢ 𝑧
5		cC	⊢ 𝐶
6		cD	⊢ 𝐷
7	0 2 4 1 3 5 6	cmpt3	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 )
8		vs	⊢ 𝑠
9		vt	⊢ 𝑡
10	8	cv	⊢ 𝑠
11	0	cv	⊢ 𝑥
12	2	cv	⊢ 𝑦
13	4	cv	⊢ 𝑧
14	11 12 13	cotp	⊢ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩
15	10 14	wceq	⊢ 𝑠 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩
16	9	cv	⊢ 𝑡
17	16 6	wceq	⊢ 𝑡 = 𝐷
18	15 17	wa	⊢ ( 𝑠 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 )
19	18 4 5	wrex	⊢ ∃ 𝑧 ∈ 𝐶 ( 𝑠 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 )
20	19 2 3	wrex	⊢ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑠 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 )
21	20 0 1	wrex	⊢ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑠 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 )
22	21 8 9	copab	⊢ { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑠 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) }
23	7 22	wceq	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 ) = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑠 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝑡 = 𝐷 ) }