Definition df-ldil 38045

Description: Define set of all lattice dilations. Similar to definition of dilation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)

Assertion

Ref	Expression
df-ldil	⊢ LDil = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ (LAut‘𝑘) ∣ ∀𝑥 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)}))

Distinct variable group:   𝑤,𝑘,𝑓,𝑥

Detailed syntax breakdown of Definition df-ldil

Step	Hyp	Ref	Expression
1		cldil 38041	. 2 class LDil
2		vk	. . 3 setvar 𝑘
3		cvv 3422	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 37925	. . . . 5 class LHyp
7	5, 6	cfv 6418	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . . . . . 9 setvar 𝑥
9	8	cv 1538	. . . . . . . 8 class 𝑥
10	4	cv 1538	. . . . . . . 8 class 𝑤
11		cple 16895	. . . . . . . . 9 class le
12	5, 11	cfv 6418	. . . . . . . 8 class (le‘𝑘)
13	9, 10, 12	wbr 5070	. . . . . . 7 wff 𝑥(le‘𝑘)𝑤
14		vf	. . . . . . . . . 10 setvar 𝑓
15	14	cv 1538	. . . . . . . . 9 class 𝑓
16	9, 15	cfv 6418	. . . . . . . 8 class (𝑓‘𝑥)
17	16, 9	wceq 1539	. . . . . . 7 wff (𝑓‘𝑥) = 𝑥
18	13, 17	wi 4	. . . . . 6 wff (𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)
19		cbs 16840	. . . . . . 7 class Base
20	5, 19	cfv 6418	. . . . . 6 class (Base‘𝑘)
21	18, 8, 20	wral 3063	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)
22		claut 37926	. . . . . 6 class LAut
23	5, 22	cfv 6418	. . . . 5 class (LAut‘𝑘)
24	21, 14, 23	crab 3067	. . . 4 class {𝑓 ∈ (LAut‘𝑘) ∣ ∀𝑥 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)}
25	4, 7, 24	cmpt 5153	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ (LAut‘𝑘) ∣ ∀𝑥 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)})
26	2, 3, 25	cmpt 5153	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ (LAut‘𝑘) ∣ ∀𝑥 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)}))
27	1, 26	wceq 1539	1 wff LDil = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ (LAut‘𝑘) ∣ ∀𝑥 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)}))

This definition is referenced by:  ldilfset  38049