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 38860
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 38856 . 2 class LAut
2 vk . . 3 setvar π‘˜
3 cvv 3475 . . 3 class V
42cv 1541 . . . . . . 7 class π‘˜
5 cbs 17144 . . . . . . 7 class Base
64, 5cfv 6544 . . . . . 6 class (Baseβ€˜π‘˜)
7 vf . . . . . . 7 setvar 𝑓
87cv 1541 . . . . . 6 class 𝑓
96, 6, 8wf1o 6543 . . . . 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 17204 . . . . . . . . . 10 class le
154, 14cfv 6544 . . . . . . . . 9 class (leβ€˜π‘˜)
1611, 13, 15wbr 5149 . . . . . . . 8 wff π‘₯(leβ€˜π‘˜)𝑦
1711, 8cfv 6544 . . . . . . . . 9 class (π‘“β€˜π‘₯)
1813, 8cfv 6544 . . . . . . . . 9 class (π‘“β€˜π‘¦)
1917, 18, 15wbr 5149 . . . . . . . 8 wff (π‘“β€˜π‘₯)(leβ€˜π‘˜)(π‘“β€˜π‘¦)
2016, 19wb 205 . . . . . . 7 wff (π‘₯(leβ€˜π‘˜)𝑦 ↔ (π‘“β€˜π‘₯)(leβ€˜π‘˜)(π‘“β€˜π‘¦))
2120, 12, 6wral 3062 . . . . . 6 wff βˆ€π‘¦ ∈ (Baseβ€˜π‘˜)(π‘₯(leβ€˜π‘˜)𝑦 ↔ (π‘“β€˜π‘₯)(leβ€˜π‘˜)(π‘“β€˜π‘¦))
2221, 10, 6wral 3062 . . . . 5 wff βˆ€π‘₯ ∈ (Baseβ€˜π‘˜)βˆ€π‘¦ ∈ (Baseβ€˜π‘˜)(π‘₯(leβ€˜π‘˜)𝑦 ↔ (π‘“β€˜π‘₯)(leβ€˜π‘˜)(π‘“β€˜π‘¦))
239, 22wa 397 . . . 4 wff (𝑓:(Baseβ€˜π‘˜)–1-1-ontoβ†’(Baseβ€˜π‘˜) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘˜)βˆ€π‘¦ ∈ (Baseβ€˜π‘˜)(π‘₯(leβ€˜π‘˜)𝑦 ↔ (π‘“β€˜π‘₯)(leβ€˜π‘˜)(π‘“β€˜π‘¦)))
2423, 7cab 2710 . . 3 class {𝑓 ∣ (𝑓:(Baseβ€˜π‘˜)–1-1-ontoβ†’(Baseβ€˜π‘˜) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘˜)βˆ€π‘¦ ∈ (Baseβ€˜π‘˜)(π‘₯(leβ€˜π‘˜)𝑦 ↔ (π‘“β€˜π‘₯)(leβ€˜π‘˜)(π‘“β€˜π‘¦)))}
252, 3, 24cmpt 5232 . 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  38953
  Copyright terms: Public domain W3C validator