Definition df-unit

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cui	⊢ Unit
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		cdsr	⊢ ∥r
4	1	cv	⊢ 𝑤
5	4 3	cfv	⊢ ( ∥r ‘ 𝑤 )
6		coppr	⊢ oppr
7	4 6	cfv	⊢ ( oppr ‘ 𝑤 )
8	7 3	cfv	⊢ ( ∥r ‘ ( oppr ‘ 𝑤 ) )
9	5 8	cin	⊢ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) )
10	9	ccnv	⊢ ◡ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) )
11		cur	⊢ 1r
12	4 11	cfv	⊢ ( 1r ‘ 𝑤 )
13	12	csn	⊢ { ( 1r ‘ 𝑤 ) }
14	10 13	cima	⊢ ( ◡ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) ) “ { ( 1r ‘ 𝑤 ) } )
15	1 2 14	cmpt	⊢ ( 𝑤 ∈ V ↦ ( ◡ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) ) “ { ( 1r ‘ 𝑤 ) } ) )
16	0 15	wceq	⊢ Unit = ( 𝑤 ∈ V ↦ ( ◡ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) ) “ { ( 1r ‘ 𝑤 ) } ) )