Definition df-laut

Description: Define set of lattice autoisomorphisms. (Contributed by NM, 11-May-2012)

	Ref	Expression
Assertion	df-laut	$$⊢\mathrm{LAut}=\left(k\in \mathrm{V}⟼\left\{f|\left(f:{\mathrm{Base}}_k\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k\wedge \forall x\in {\mathrm{Base}}_k\forall y\in {\mathrm{Base}}_k\left(x{\le }_{k}y\leftrightarrow f\left(x\right){\le }_{k}f\left(y\right)\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		claut	$$class\mathrm{LAut}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4	3	cv	$$setvarf$$
5		cbs	$$class\mathrm{Base}$$
6	1	cv	$$setvark$$
7	6 5	cfv	$$class{\mathrm{Base}}_k$$
8	7 7 4	wf1o	$$wfff:{\mathrm{Base}}_k\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k$$
9		vx	$$setvarx$$
10		vy	$$setvary$$
11	9	cv	$$setvarx$$
12		cple	$$class\mathrm{le}$$
13	6 12	cfv	$$class{\le }_k$$
14	10	cv	$$setvary$$
15	11 14 13	wbr	$$wffx{\le }_{k}y$$
16	11 4	cfv	$$classf\left(x\right)$$
17	14 4	cfv	$$classf\left(y\right)$$
18	16 17 13	wbr	$$wfff\left(x\right){\le }_{k}f\left(y\right)$$
19	15 18	wb	$$wff\left(x{\le }_{k}y\leftrightarrow f\left(x\right){\le }_{k}f\left(y\right)\right)$$
20	19 10 7	wral	$$wff\forall y\in {\mathrm{Base}}_k\left(x{\le }_{k}y\leftrightarrow f\left(x\right){\le }_{k}f\left(y\right)\right)$$
21	20 9 7	wral	$$wff\forall x\in {\mathrm{Base}}_k\forall y\in {\mathrm{Base}}_k\left(x{\le }_{k}y\leftrightarrow f\left(x\right){\le }_{k}f\left(y\right)\right)$$
22	8 21	wa	$$wff\left(f:{\mathrm{Base}}_k\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k\wedge \forall x\in {\mathrm{Base}}_k\forall y\in {\mathrm{Base}}_k\left(x{\le }_{k}y\leftrightarrow f\left(x\right){\le }_{k}f\left(y\right)\right)\right)$$
23	22 3	cab	$$class\left\{f|\left(f:{\mathrm{Base}}_k\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k\wedge \forall x\in {\mathrm{Base}}_k\forall y\in {\mathrm{Base}}_k\left(x{\le }_{k}y\leftrightarrow f\left(x\right){\le }_{k}f\left(y\right)\right)\right)\right\}$$
24	1 2 23	cmpt	$$class\left(k\in \mathrm{V}⟼\left\{f|\left(f:{\mathrm{Base}}_k\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k\wedge \forall x\in {\mathrm{Base}}_k\forall y\in {\mathrm{Base}}_k\left(x{\le }_{k}y\leftrightarrow f\left(x\right){\le }_{k}f\left(y\right)\right)\right)\right\}\right)$$
25	0 24	wceq	$$wff\mathrm{LAut}=\left(k\in \mathrm{V}⟼\left\{f|\left(f:{\mathrm{Base}}_k\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k\wedge \forall x\in {\mathrm{Base}}_k\forall y\in {\mathrm{Base}}_k\left(x{\le }_{k}y\leftrightarrow f\left(x\right){\le }_{k}f\left(y\right)\right)\right)\right\}\right)$$