Theorem islaut

Description: The predictate "is a lattice automorphism." (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	islaut	$$⊢K\in A\to \left(F\in I\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)$$

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	1 2 3	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\}$$
5	4	eleq2d	$$⊢K\in A\to \left(F\in I\leftrightarrow F\in \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\}\right)$$
6		f1of	$$⊢F:B\underset{1-1\; onto}{⟶}B\to F:B⟶B$$
7	1	fvexi	$$⊢B\in \mathrm{V}$$
8		fex	$$⊢\left(F:B⟶B\wedge B\in \mathrm{V}\right)\to F\in \mathrm{V}$$
9	6 7 8	sylancl	$$⊢F:B\underset{1-1\; onto}{⟶}B\to F\in \mathrm{V}$$
10	9	adantr	$$⊢\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\in \mathrm{V}$$
11		f1oeq1	$$⊢f=F\to \left(f:B\underset{1-1\; onto}{⟶}B\leftrightarrow F:B\underset{1-1\; onto}{⟶}B\right)$$
12		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
13		fveq1	$$⊢f=F\to f\left(y\right)=F\left(y\right)$$
14	12 13	breq12d	$$⊢f=F\to \left(f\left(x\right)\underset{\dot{}}{\le }f\left(y\right)\leftrightarrow F\left(x\right)\underset{\dot{}}{\le }F\left(y\right)\right)$$
15	14	bibi2d	$$⊢f=F\to \left(\left(x\underset{\dot{}}{\le }y\leftrightarrow f\left(x\right)\underset{\dot{}}{\le }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	15	2ralbidv	$$⊢f=F\to \left(\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)\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)$$
17	11 16	anbi12d	$$⊢f=F\to \left(\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)\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)$$
18	10 17	elab3	$$⊢F\in \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\}\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)$$
19	5 18	bitrdi	$$⊢K\in A\to \left(F\in I\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)$$