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

Definition df-laut 37658
Description: Define set of lattice autoisomorphisms. (Contributed by NM, 11-May-2012.)
Assertion
Ref Expression
df-laut LAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓𝑥)(le‘𝑘)(𝑓𝑦)))})
Distinct variable group:   𝑓,𝑘,𝑥,𝑦

Detailed syntax breakdown of Definition df-laut
StepHypRef Expression
1 claut 37654 . 2 class LAut
2 vk . . 3 setvar 𝑘
3 cvv 3400 . . 3 class V
42cv 1541 . . . . . . 7 class 𝑘
5 cbs 16598 . . . . . . 7 class Base
64, 5cfv 6349 . . . . . 6 class (Base‘𝑘)
7 vf . . . . . . 7 setvar 𝑓
87cv 1541 . . . . . 6 class 𝑓
96, 6, 8wf1o 6348 . . . . 5 wff 𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘)
10 vx . . . . . . . . . 10 setvar 𝑥
1110cv 1541 . . . . . . . . 9 class 𝑥
12 vy . . . . . . . . . 10 setvar 𝑦
1312cv 1541 . . . . . . . . 9 class 𝑦
14 cple 16687 . . . . . . . . . 10 class le
154, 14cfv 6349 . . . . . . . . 9 class (le‘𝑘)
1611, 13, 15wbr 5040 . . . . . . . 8 wff 𝑥(le‘𝑘)𝑦
1711, 8cfv 6349 . . . . . . . . 9 class (𝑓𝑥)
1813, 8cfv 6349 . . . . . . . . 9 class (𝑓𝑦)
1917, 18, 15wbr 5040 . . . . . . . 8 wff (𝑓𝑥)(le‘𝑘)(𝑓𝑦)
2016, 19wb 209 . . . . . . 7 wff (𝑥(le‘𝑘)𝑦 ↔ (𝑓𝑥)(le‘𝑘)(𝑓𝑦))
2120, 12, 6wral 3054 . . . . . 6 wff 𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓𝑥)(le‘𝑘)(𝑓𝑦))
2221, 10, 6wral 3054 . . . . 5 wff 𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓𝑥)(le‘𝑘)(𝑓𝑦))
239, 22wa 399 . . . 4 wff (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓𝑥)(le‘𝑘)(𝑓𝑦)))
2423, 7cab 2717 . . 3 class {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓𝑥)(le‘𝑘)(𝑓𝑦)))}
252, 3, 24cmpt 5120 . 2 class (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓𝑥)(le‘𝑘)(𝑓𝑦)))})
261, 25wceq 1542 1 wff LAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓𝑥)(le‘𝑘)(𝑓𝑦)))})
Colors of variables: wff setvar class
This definition is referenced by:  lautset  37751
  Copyright terms: Public domain W3C validator