df-mpo

Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x , y (in A X. B ) to C ( x , y ) ". An extension of df-mpt for two arguments. (Contributed by NM, 17-Feb-2008)

		Ref	Expression
	Assertion	df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		vy	⊢ 𝑦
3		cB	⊢ 𝐵
4		cC	⊢ 𝐶
5	0 2 1 3 4	cmpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
6		vz	⊢ 𝑧
7	0	cv	⊢ 𝑥
8	7 1	wcel	⊢ 𝑥 ∈ 𝐴
9	2	cv	⊢ 𝑦
10	9 3	wcel	⊢ 𝑦 ∈ 𝐵
11	8 10	wa	⊢ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
12	6	cv	⊢ 𝑧
13	12 4	wceq	⊢ 𝑧 = 𝐶
14	11 13	wa	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 )
15	14 0 2 6	coprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
16	5 15	wceq	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }

Metamath Proof Explorer

Definition df-mpo

Detailed syntax breakdown