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∈yz=uov

Detailed syntax breakdown

Step Hyp Ref Expression
0 celwise classelwise
1 vo setvaro
2 cvv classV
3 vx setvarx
4 vy setvary
5 vz setvarz
6 vu setvaru
7 3 cv setvarx
8 vv setvarv
9 4 cv setvary
10 5 cv setvarz
11 6 cv setvaru
12 1 cv setvaro
13 8 cv setvarv
14 11 13 12 co classuov
15 10 14 wceq wffz=uov
16 15 8 9 wrex wff∃v∈yz=uov
17 16 6 7 wrex wff∃u∈x∃v∈yz=uov
18 17 5 cab classz|∃u∈x∃v∈yz=uov
19 3 4 2 2 18 cmpo classx∈V,y∈V⟼z|∃u∈x∃v∈yz=uov
20 1 2 19 cmpt classo∈V⟼x∈V,y∈V⟼z|∃u∈x∃v∈yz=uov
21 0 20 wceq wffelwise=o∈V⟼x∈V,y∈V⟼z|∃u∈x∃v∈yz=uov