Definition df-laut 35275

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

Assertion

Ref	Expression
df-laut	|- LAut = ( k e. _V |-> { f | ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) /\ A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) ) } )

Distinct variable group:   f, k, x, y

Detailed syntax breakdown of Definition df-laut

Step	Hyp	Ref	Expression
1		claut 35271	. 2 class LAut
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . . . 7 class k
5		cbs 15857	. . . . . . 7 class Base
6	4, 5	cfv 5888	. . . . . 6 class ( Base ` k )
7		vf	. . . . . . 7 setvar f
8	7	cv 1482	. . . . . 6 class f
9	6, 6, 8	wf1o 5887	. . . . 5 wff f : ( Base ` k ) -1-1-onto-> ( Base ` k )
10		vx	. . . . . . . . . 10 setvar x
11	10	cv 1482	. . . . . . . . 9 class x
12		vy	. . . . . . . . . 10 setvar y
13	12	cv 1482	. . . . . . . . 9 class y
14		cple 15948	. . . . . . . . . 10 class le
15	4, 14	cfv 5888	. . . . . . . . 9 class ( le ` k )
16	11, 13, 15	wbr 4653	. . . . . . . 8 wff x ( le ` k ) y
17	11, 8	cfv 5888	. . . . . . . . 9 class ( f ` x )
18	13, 8	cfv 5888	. . . . . . . . 9 class ( f ` y )
19	17, 18, 15	wbr 4653	. . . . . . . 8 wff ( f ` x ) ( le ` k ) ( f ` y )
20	16, 19	wb 196	. . . . . . 7 wff ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) )
21	20, 12, 6	wral 2912	. . . . . 6 wff A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) )
22	21, 10, 6	wral 2912	. . . . 5 wff A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) )
23	9, 22	wa 384	. . . 4 wff ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) /\ A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) )
24	23, 7	cab 2608	. . 3 class { f | ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) /\ A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) ) }
25	2, 3, 24	cmpt 4729	. 2 class ( k e. _V |-> { f | ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) /\ A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) ) } )
26	1, 25	wceq 1483	1 wff LAut = ( k e. _V |-> { f | ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) /\ A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) ) } )

This definition is referenced by:  lautset  35368