Definition df-unit 13257

Description: Define the set of units in a ring, that is, all elements with a left and right multiplicative inverse. (Contributed by Mario Carneiro, 1-Dec-2014.)

Assertion

Ref	Expression
df-unit	⊢ Unit = (𝑤 ∈ V ↦ (◡((∥r‘𝑤) ∩ (∥r‘(oppr‘𝑤))) “ {(1r‘𝑤)}))

Detailed syntax breakdown of Definition df-unit

Step	Hyp	Ref	Expression
1		cui 13254	. 2 class Unit
2		vw	. . 3 setvar 𝑤
3		cvv 2737	. . 3 class V
4	2	cv 1352	. . . . . . 7 class 𝑤
5		cdsr 13253	. . . . . . 7 class ∥r
6	4, 5	cfv 5216	. . . . . 6 class (∥r‘𝑤)
7		coppr 13237	. . . . . . . 8 class oppr
8	4, 7	cfv 5216	. . . . . . 7 class (oppr‘𝑤)
9	8, 5	cfv 5216	. . . . . 6 class (∥r‘(oppr‘𝑤))
10	6, 9	cin 3128	. . . . 5 class ((∥r‘𝑤) ∩ (∥r‘(oppr‘𝑤)))
11	10	ccnv 4625	. . . 4 class ◡((∥r‘𝑤) ∩ (∥r‘(oppr‘𝑤)))
12		cur 13140	. . . . . 6 class 1r
13	4, 12	cfv 5216	. . . . 5 class (1r‘𝑤)
14	13	csn 3592	. . . 4 class {(1r‘𝑤)}
15	11, 14	cima 4629	. . 3 class (◡((∥r‘𝑤) ∩ (∥r‘(oppr‘𝑤))) “ {(1r‘𝑤)})
16	2, 3, 15	cmpt 4064	. 2 class (𝑤 ∈ V ↦ (◡((∥r‘𝑤) ∩ (∥r‘(oppr‘𝑤))) “ {(1r‘𝑤)}))
17	1, 16	wceq 1353	1 wff Unit = (𝑤 ∈ V ↦ (◡((∥r‘𝑤) ∩ (∥r‘(oppr‘𝑤))) “ {(1r‘𝑤)}))

This definition is referenced by:  isunitd  13273