Metamath Proof Explorer

Definition df-elwise

Description: Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers ( axaddf ), so if A and B are sets of complex numbers, then ( A ( elwise+ ) B ) is the set of numbers of the form ( x + y ) with x e. A and y e. B . The set of odd natural numbers is ( ( { 2 } ( elwisex. ) NN0 ) ( elwise+ ) { 1 } ) , or less formally 2 NN0 + 1 . (Contributed by BJ, 22-Dec-2021)

Ref Expression
Assertion df-elwise ⊢ elwise = o ∈ V ⟼ x ∈ V , y ∈ V ⟼ z | ∃ u ∈ x ∃ v ∈ y z = u o v

Detailed syntax breakdown

Step Hyp Ref Expression
0 celwise class elwise
1 vo setvar o
2 cvv class V
3 vx setvar x
4 vy setvar y
5 vz setvar z
6 vu setvar u
7 3 cv setvar x
8 vv setvar v
9 4 cv setvar y
10 5 cv setvar z
11 6 cv setvar u
12 1 cv setvar o
13 8 cv setvar v
14 11 13 12 co class u o v
15 10 14 wceq wff z = u o v
16 15 8 9 wrex wff ∃ v ∈ y z = u o v
17 16 6 7 wrex wff ∃ u ∈ x ∃ v ∈ y z = u o v
18 17 5 cab class z | ∃ u ∈ x ∃ v ∈ y z = u o v
19 3 4 2 2 18 cmpo class x ∈ V , y ∈ V ⟼ z | ∃ u ∈ x ∃ v ∈ y z = u o v
20 1 2 19 cmpt class o ∈ V ⟼ x ∈ V , y ∈ V ⟼ z | ∃ u ∈ x ∃ v ∈ y z = u o v
21 0 20 wceq wff elwise = o ∈ V ⟼ x ∈ V , y ∈ V ⟼ z | ∃ u ∈ x ∃ v ∈ y z = u o v