Definition df-rq

Description: Define reciprocal on positive fractions. It means the same thing as one divided by the argument (although we don't define full division since we will never need it). This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-2.5 of Gleason p. 119, who uses an asterisk to denote this unary operation. (Contributed by NM, 6-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	df-rq	⊢ *Q = ( ◡ ·Q “ { 1Q } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crq	⊢ *Q
1		cmq	⊢ ·Q
2	1	ccnv	⊢ ◡ ·Q
3		c1q	⊢ 1Q
4	3	csn	⊢ { 1Q }
5	2 4	cima	⊢ ( ◡ ·Q “ { 1Q } )
6	0 5	wceq	⊢ *Q = ( ◡ ·Q “ { 1Q } )