Metamath Proof Explorer

Definition df-laut

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

Ref Expression
Assertion 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 claut 
 |-  LAut
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vf 
 |-  f
4 3 cv 
 |-  f
5 cbs 
 |-  Base
6 1 cv 
 |-  k
7 6 5 cfv 
 |-  ( Base ` k )
8 7 7 4 wf1o 
 |-  f : ( Base ` k ) -1-1-onto-> ( Base ` k )
9 vx 
 |-  x
10 vy 
 |-  y
11 9 cv 
 |-  x
12 cple 
 |-  le
13 6 12 cfv 
 |-  ( le ` k )
14 10 cv 
 |-  y
15 11 14 13 wbr 
 |-  x ( le ` k ) y
16 11 4 cfv 
 |-  ( f ` x )
17 14 4 cfv 
 |-  ( f ` y )
18 16 17 13 wbr 
 |-  ( f ` x ) ( le ` k ) ( f ` y )
19 15 18 wb 
 |-  ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) )
20 19 10 7 wral 
 |-  A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) )
21 20 9 7 wral 
 |-  A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) )
22 8 21 wa 
 |-  ( 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 ) ) )
23 22 3 cab 
 |-  { 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 ) ) ) }
24 1 2 23 cmpt 
 |-  ( 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 ) ) ) } )
25 0 24 wceq 
 |-  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 ) ) ) } )