Definition df-laut 39163

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

Step	Hyp	Ref	Expression
1		claut 39159	. 2 class LAut
2		vk	. . 3 setvar 𝑘
3		cvv 3472	. . 3 class V
4	2	cv 1538	. . . . . . 7 class 𝑘
5		cbs 17148	. . . . . . 7 class Base
6	4, 5	cfv 6542	. . . . . 6 class (Base‘𝑘)
7		vf	. . . . . . 7 setvar 𝑓
8	7	cv 1538	. . . . . 6 class 𝑓
9	6, 6, 8	wf1o 6541	. . . . 5 wff 𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘)
10		vx	. . . . . . . . . 10 setvar 𝑥
11	10	cv 1538	. . . . . . . . 9 class 𝑥
12		vy	. . . . . . . . . 10 setvar 𝑦
13	12	cv 1538	. . . . . . . . 9 class 𝑦
14		cple 17208	. . . . . . . . . 10 class le
15	4, 14	cfv 6542	. . . . . . . . 9 class (le‘𝑘)
16	11, 13, 15	wbr 5147	. . . . . . . 8 wff 𝑥(le‘𝑘)𝑦
17	11, 8	cfv 6542	. . . . . . . . 9 class (𝑓‘𝑥)
18	13, 8	cfv 6542	. . . . . . . . 9 class (𝑓‘𝑦)
19	17, 18, 15	wbr 5147	. . . . . . . 8 wff (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)
20	16, 19	wb 205	. . . . . . 7 wff (𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦))
21	20, 12, 6	wral 3059	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦))
22	21, 10, 6	wral 3059	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦))
23	9, 22	wa 394	. . . 4 wff (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))
24	23, 7	cab 2707	. . 3 class {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))}
25	2, 3, 24	cmpt 5230	. 2 class (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))})
26	1, 25	wceq 1539	1 wff LAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))})

This definition is referenced by:  lautset  39256