Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-laut Unicode version

Definition df-laut 30800
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
StepHypRef Expression
1 claut 30796 . 2  class  LAut
2 vk . . 3  set  k
3 cvv 2801 . . 3  class  _V
42cv 1631 . . . . . . 7  class  k
5 cbs 13164 . . . . . . 7  class  Base
64, 5cfv 5271 . . . . . 6  class  ( Base `  k )
7 vf . . . . . . 7  set  f
87cv 1631 . . . . . 6  class  f
96, 6, 8wf1o 5270 . . . . 5  wff  f : ( Base `  k
)
-1-1-onto-> ( Base `  k )
10 vx . . . . . . . . . 10  set  x
1110cv 1631 . . . . . . . . 9  class  x
12 vy . . . . . . . . . 10  set  y
1312cv 1631 . . . . . . . . 9  class  y
14 cple 13231 . . . . . . . . . 10  class  le
154, 14cfv 5271 . . . . . . . . 9  class  ( le
`  k )
1611, 13, 15wbr 4039 . . . . . . . 8  wff  x ( le `  k ) y
1711, 8cfv 5271 . . . . . . . . 9  class  ( f `
 x )
1813, 8cfv 5271 . . . . . . . . 9  class  ( f `
 y )
1917, 18, 15wbr 4039 . . . . . . . 8  wff  ( f `
 x ) ( le `  k ) ( f `  y
)
2016, 19wb 176 . . . . . . 7  wff  ( x ( le `  k
) y  <->  ( f `  x ) ( le
`  k ) ( f `  y ) )
2120, 12, 6wral 2556 . . . . . 6  wff  A. y  e.  ( Base `  k
) ( x ( le `  k ) y  <->  ( f `  x ) ( le
`  k ) ( f `  y ) )
2221, 10, 6wral 2556 . . . . 5  wff  A. x  e.  ( Base `  k
) A. y  e.  ( Base `  k
) ( x ( le `  k ) y  <->  ( f `  x ) ( le
`  k ) ( f `  y ) )
239, 22wa 358 . . . 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 ) ) )
2423, 7cab 2282 . . 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 ) ) ) }
252, 3, 24cmpt 4093 . 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 ) ) ) } )
261, 25wceq 1632 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 ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  lautset  30893
  Copyright terms: Public domain W3C validator