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 = ( 𝑜 ∈ V ↦ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∣ ∃ 𝑢 ∈ 𝑥 ∃ 𝑣 ∈ 𝑦 𝑧 = ( 𝑢 𝑜 𝑣 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		celwise	⊢ elwise
1		vo	⊢ 𝑜
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		vy	⊢ 𝑦
5		vz	⊢ 𝑧
6		vu	⊢ 𝑢
7	3	cv	⊢ 𝑥
8		vv	⊢ 𝑣
9	4	cv	⊢ 𝑦
10	5	cv	⊢ 𝑧
11	6	cv	⊢ 𝑢
12	1	cv	⊢ 𝑜
13	8	cv	⊢ 𝑣
14	11 13 12	co	⊢ ( 𝑢 𝑜 𝑣 )
15	10 14	wceq	⊢ 𝑧 = ( 𝑢 𝑜 𝑣 )
16	15 8 9	wrex	⊢ ∃ 𝑣 ∈ 𝑦 𝑧 = ( 𝑢 𝑜 𝑣 )
17	16 6 7	wrex	⊢ ∃ 𝑢 ∈ 𝑥 ∃ 𝑣 ∈ 𝑦 𝑧 = ( 𝑢 𝑜 𝑣 )
18	17 5	cab	⊢ { 𝑧 ∣ ∃ 𝑢 ∈ 𝑥 ∃ 𝑣 ∈ 𝑦 𝑧 = ( 𝑢 𝑜 𝑣 ) }
19	3 4 2 2 18	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∣ ∃ 𝑢 ∈ 𝑥 ∃ 𝑣 ∈ 𝑦 𝑧 = ( 𝑢 𝑜 𝑣 ) } )
20	1 2 19	cmpt	⊢ ( 𝑜 ∈ V ↦ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∣ ∃ 𝑢 ∈ 𝑥 ∃ 𝑣 ∈ 𝑦 𝑧 = ( 𝑢 𝑜 𝑣 ) } ) )
21	0 20	wceq	⊢ elwise = ( 𝑜 ∈ V ↦ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∣ ∃ 𝑢 ∈ 𝑥 ∃ 𝑣 ∈ 𝑦 𝑧 = ( 𝑢 𝑜 𝑣 ) } ) )