Definition df-com2 32959

Description: A device to add commutativity to various sorts of rings. I use ran 𝑔 because I suppose 𝑔 has a neutral element and therefore is onto. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)

Assertion

Ref	Expression
df-com2	⊢ Com2 = {⟨𝑔, ℎ⟩ ∣ ∀𝑎 ∈ ran 𝑔∀𝑏 ∈ ran 𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎)}

Distinct variable group:   𝑔,ℎ,𝑎,𝑏

Detailed syntax breakdown of Definition df-com2

Step	Hyp	Ref	Expression
1		ccm2 32958	. 2 class Com2
2		va	. . . . . . . 8 setvar 𝑎
3	2	cv 1474	. . . . . . 7 class 𝑎
4		vb	. . . . . . . 8 setvar 𝑏
5	4	cv 1474	. . . . . . 7 class 𝑏
6		vh	. . . . . . . 8 setvar ℎ
7	6	cv 1474	. . . . . . 7 class ℎ
8	3, 5, 7	co 6549	. . . . . 6 class (𝑎ℎ𝑏)
9	5, 3, 7	co 6549	. . . . . 6 class (𝑏ℎ𝑎)
10	8, 9	wceq 1475	. . . . 5 wff (𝑎ℎ𝑏) = (𝑏ℎ𝑎)
11		vg	. . . . . . 7 setvar 𝑔
12	11	cv 1474	. . . . . 6 class 𝑔
13	12	crn 5039	. . . . 5 class ran 𝑔
14	10, 4, 13	wral 2896	. . . 4 wff ∀𝑏 ∈ ran 𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎)
15	14, 2, 13	wral 2896	. . 3 wff ∀𝑎 ∈ ran 𝑔∀𝑏 ∈ ran 𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎)
16	15, 11, 6	copab 4642	. 2 class {⟨𝑔, ℎ⟩ ∣ ∀𝑎 ∈ ran 𝑔∀𝑏 ∈ ran 𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎)}
17	1, 16	wceq 1475	1 wff Com2 = {⟨𝑔, ℎ⟩ ∣ ∀𝑎 ∈ ran 𝑔∀𝑏 ∈ ran 𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎)}

This definition is referenced by:  iscom2  32964