Definition df-elwise 35230

Description: Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 10885), so if 𝐴 and 𝐵 are sets of complex numbers, then (𝐴(elwise‘ + )𝐵) is the set of numbers of the form (𝑥 + 𝑦) with 𝑥 ∈ 𝐴 and 𝑦 ∈ 𝐵. The set of odd natural numbers is (({2}(elwise‘ · )ℕ₀)(elwise‘ + ){1}), or less formally 2ℕ₀ + 1. (Contributed by BJ, 22-Dec-2021.)

Assertion

Ref	Expression
df-elwise	⊢ elwise = (𝑜 ∈ V ↦ (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)}))

Distinct variable group:   𝑥,𝑜,𝑦,𝑧,𝑢,𝑣

Detailed syntax breakdown of Definition df-elwise

Step	Hyp	Ref	Expression
1		celwise 35229	. 2 class elwise
2		vo	. . 3 setvar 𝑜
3		cvv 3430	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6		vz	. . . . . . . . 9 setvar 𝑧
7	6	cv 1540	. . . . . . . 8 class 𝑧
8		vu	. . . . . . . . . 10 setvar 𝑢
9	8	cv 1540	. . . . . . . . 9 class 𝑢
10		vv	. . . . . . . . . 10 setvar 𝑣
11	10	cv 1540	. . . . . . . . 9 class 𝑣
12	2	cv 1540	. . . . . . . . 9 class 𝑜
13	9, 11, 12	co 7268	. . . . . . . 8 class (𝑢𝑜𝑣)
14	7, 13	wceq 1541	. . . . . . 7 wff 𝑧 = (𝑢𝑜𝑣)
15	5	cv 1540	. . . . . . 7 class 𝑦
16	14, 10, 15	wrex 3066	. . . . . 6 wff ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)
17	4	cv 1540	. . . . . 6 class 𝑥
18	16, 8, 17	wrex 3066	. . . . 5 wff ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)
19	18, 6	cab 2716	. . . 4 class {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)}
20	4, 5, 3, 3, 19	cmpo 7270	. . 3 class (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)})
21	2, 3, 20	cmpt 5161	. 2 class (𝑜 ∈ V ↦ (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)}))
22	1, 21	wceq 1541	1 wff elwise = (𝑜 ∈ V ↦ (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)}))

This definition is referenced by: (None)