Definition df-staf

Description: Define the functionalization of the involution in a star ring. This is not strictly necessary but by having *r as an actual function we can state the principal properties of an involution much more cleanly. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Assertion	df-staf	$$⊢{\ast }_{\mathrm{𝑟𝑓}}=\left(f\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_f⟼x^{{\mathrm{*}}_f}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstf	$$class{\ast }_{\mathrm{𝑟𝑓}}$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarf$$
6	5 4	cfv	$$class{\mathrm{Base}}_f$$
7		cstv	$$class{\ast }_{𝑟}$$
8	5 7	cfv	$$class{\mathrm{*}}_f$$
9	3	cv	$$setvarx$$
10	9 8	cfv	$$class{x}^{{\mathrm{*}}_f}$$
11	3 6 10	cmpt	$$class\left(x\in {\mathrm{Base}}_f⟼x^{{\mathrm{*}}_f}\right)$$
12	1 2 11	cmpt	$$class\left(f\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_f⟼x^{{\mathrm{*}}_f}\right)\right)$$
13	0 12	wceq	$$wff{\ast }_{\mathrm{𝑟𝑓}}=\left(f\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_f⟼x^{{\mathrm{*}}_f}\right)\right)$$