Definition df-ldil 38125

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 38121	. 2 class LDil
2		vk	. . 3 setvar 𝑘
3		cvv 3433	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 38005	. . . . 5 class LHyp
7	5, 6	cfv 6437	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . . . . . 9 setvar 𝑥
9	8	cv 1538	. . . . . . . 8 class 𝑥
10	4	cv 1538	. . . . . . . 8 class 𝑤
11		cple 16978	. . . . . . . . 9 class le
12	5, 11	cfv 6437	. . . . . . . 8 class (le‘𝑘)
13	9, 10, 12	wbr 5075	. . . . . . 7 wff 𝑥(le‘𝑘)𝑤
14		vf	. . . . . . . . . 10 setvar 𝑓
15	14	cv 1538	. . . . . . . . 9 class 𝑓
16	9, 15	cfv 6437	. . . . . . . 8 class (𝑓‘𝑥)
17	16, 9	wceq 1539	. . . . . . 7 wff (𝑓‘𝑥) = 𝑥
18	13, 17	wi 4	. . . . . 6 wff (𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)
19		cbs 16921	. . . . . . 7 class Base
20	5, 19	cfv 6437	. . . . . 6 class (Base‘𝑘)
21	18, 8, 20	wral 3065	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)
22		claut 38006	. . . . . 6 class LAut
23	5, 22	cfv 6437	. . . . 5 class (LAut‘𝑘)
24	21, 14, 23	crab 3069	. . . 4 class {𝑓 ∈ (LAut‘𝑘) ∣ ∀𝑥 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)}
25	4, 7, 24	cmpt 5158	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ (LAut‘𝑘) ∣ ∀𝑥 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑤 → (𝑓‘𝑥) = 𝑥)})
26	2, 3, 25	cmpt 5158	. 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  38129