Definition df-unit 13852

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 = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )

Detailed syntax breakdown of Definition df-unit

Step	Hyp	Ref	Expression
1		cui 13849	. 2 class Unit
2		vw	. . 3 setvar w
3		cvv 2772	. . 3 class _V
4	2	cv 1372	. . . . . . 7 class w
5		cdsr 13848	. . . . . . 7 class ||r
6	4, 5	cfv 5271	. . . . . 6 class ( ||r ` w )
7		coppr 13829	. . . . . . . 8 class oppr
8	4, 7	cfv 5271	. . . . . . 7 class (oppr ` w )
9	8, 5	cfv 5271	. . . . . 6 class ( ||r ` (oppr ` w ) )
10	6, 9	cin 3165	. . . . 5 class ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) )
11	10	ccnv 4674	. . . 4 class `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) )
12		cur 13721	. . . . . 6 class 1r
13	4, 12	cfv 5271	. . . . 5 class ( 1r ` w )
14	13	csn 3633	. . . 4 class { ( 1r ` w ) }
15	11, 14	cima 4678	. . 3 class ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } )
16	2, 3, 15	cmpt 4105	. 2 class ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
17	1, 16	wceq 1373	1 wff Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )

This definition is referenced by:  isunitd  13868