Theorem lautset

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

	Ref	Expression
Hypotheses	lautset.b	$$⊢B={\mathrm{Base}}_K$$
	lautset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lautset.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
Assertion	lautset	$$⊢K\in A\to I=\left\{f|\left(f:B\underset{1-1\; onto}{⟶}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lautset.b	$$⊢B={\mathrm{Base}}_K$$
2		lautset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lautset.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
4		elex	$$⊢K\in A\to K\in \mathrm{V}$$
5		fveq2	$$⊢k=K\to {\mathrm{Base}}_k={\mathrm{Base}}_K$$
6	5 1	eqtr4di	$$⊢k=K\to {\mathrm{Base}}_k=B$$
7	6	f1oeq2d	$$⊢k=K\to \left(f:{\mathrm{Base}}_k\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k\leftrightarrow f:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k\right)$$
8		f1oeq3	$$⊢{\mathrm{Base}}_k=B\to \left(f:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k\leftrightarrow f:B\underset{1-1\; onto}{⟶}B\right)$$
9	6 8	syl	$$⊢k=K\to \left(f:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k\leftrightarrow f:B\underset{1-1\; onto}{⟶}B\right)$$
10	7 9	bitrd	$$⊢k=K\to \left(f:{\mathrm{Base}}_k\underset{1-1\; onto}{⟶}{\mathrm{Base}}_k\leftrightarrow f:B\underset{1-1\; onto}{⟶}B\right)$$
11		fveq2	$$⊢k=K\to {\le }_k={\le }_K$$
12	11 2	eqtr4di	$$⊢k=K\to {\le }_k=\underset{\dot{}}{\le }$$
13	12	breqd	$$⊢k=K\to \left(x{\le }_{k}y\leftrightarrow x\underset{\dot{}}{\le }y\right)$$
14	12	breqd	$$⊢k=K\to \left(f\left(x\right){\le }_{k}f\left(y\right)\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)$$
15	13 14	bibi12d	$$⊢k=K\to \left(\left(x{\le }_{k}y\leftrightarrow f\left(x\right){\le }_{k}f\left(y\right)\right)\leftrightarrow \left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)$$
16	6 15	raleqbidv	$$⊢k=K\to \left(\forall y\in {\mathrm{Base}}_k\left(x{\le }_{k}y\leftrightarrow f\left(x\right){\le }_{k}f\left(y\right)\right)\leftrightarrow \forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)$$
17	6 16	raleqbidv	$$⊢k=K\to \left(\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)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)$$
18	10 17	anbi12d	$$⊢k=K\to \left(\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)\leftrightarrow \left(f:B\underset{1-1\; onto}{⟶}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)\right)$$
19	18	abbidv	$$⊢k=K\to \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\}=\left\{f|\left(f:B\underset{1-1\; onto}{⟶}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)\right\}$$
20		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)$$
21	1	fvexi	$$⊢B\in \mathrm{V}$$
22	21 21	mapval	$$⊢B^B=\left\{f|f:B⟶B\right\}$$
23		ovex	$$⊢B^B\in \mathrm{V}$$
24	22 23	eqeltrri	$$⊢\left\{f|f:B⟶B\right\}\in \mathrm{V}$$
25		f1of	$$⊢f:B\underset{1-1\; onto}{⟶}B\to f:B⟶B$$
26	25	ss2abi	$$⊢\left\{f|f:B\underset{1-1\; onto}{⟶}B\right\}\subseteq \left\{f|f:B⟶B\right\}$$
27	24 26	ssexi	$$⊢\left\{f|f:B\underset{1-1\; onto}{⟶}B\right\}\in \mathrm{V}$$
28		simpl	$$⊢\left(f:B\underset{1-1\; onto}{⟶}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)\to f:B\underset{1-1\; onto}{⟶}B$$
29	28	ss2abi	$$⊢\left\{f|\left(f:B\underset{1-1\; onto}{⟶}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)\right\}\subseteq \left\{f|f:B\underset{1-1\; onto}{⟶}B\right\}$$
30	27 29	ssexi	$$⊢\left\{f|\left(f:B\underset{1-1\; onto}{⟶}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)\right\}\in \mathrm{V}$$
31	19 20 30	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{LAut}\left(K\right)=\left\{f|\left(f:B\underset{1-1\; onto}{⟶}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)\right\}$$
32	3 31	eqtrid	$$⊢K\in \mathrm{V}\to I=\left\{f|\left(f:B\underset{1-1\; onto}{⟶}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)\right\}$$
33	4 32	syl	$$⊢K\in A\to I=\left\{f|\left(f:B\underset{1-1\; onto}{⟶}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\right)\right)\right\}$$