df-ldil

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

		Ref	Expression
	Assertion	df-ldil	$⊢ LDil = (k \in V ⟼ (w \in LHyp (k) ⟼ \{f \in LAut (k) \| \forall x \in {Base}_{k} (x \leq_{k} w \to f (x) = x)\}))$

Step	Hyp	Ref	Expression
0		cldil	$class LDil$
1		vk	$setvar k$
2		cvv	$class V$
3		vw	$setvar w$
4		clh	$class LHyp$
5	1	cv	$setvar k$
6	5 4	cfv	$class LHyp (k)$
7		vf	$setvar f$
8		claut	$class LAut$
9	5 8	cfv	$class LAut (k)$
10		vx	$setvar x$
11		cbs	$class Base$
12	5 11	cfv	$class {Base}_{k}$
13	10	cv	$setvar x$
14		cple	$class le$
15	5 14	cfv	$class \leq_{k}$
16	3	cv	$setvar w$
17	13 16 15	wbr	$wff x \leq_{k} w$
18	7	cv	$setvar f$
19	13 18	cfv	$class f (x)$
20	19 13	wceq	$wff f (x) = x$
21	17 20	wi	$wff (x \leq_{k} w \to f (x) = x)$
22	21 10 12	wral	$wff \forall x \in {Base}_{k} (x \leq_{k} w \to f (x) = x)$
23	22 7 9	crab	$class \{f \in LAut (k) \| \forall x \in {Base}_{k} (x \leq_{k} w \to f (x) = x)\}$
24	3 6 23	cmpt	$class (w \in LHyp (k) ⟼ \{f \in LAut (k) \| \forall x \in {Base}_{k} (x \leq_{k} w \to f (x) = x)\})$
25	1 2 24	cmpt	$class (k \in V ⟼ (w \in LHyp (k) ⟼ \{f \in LAut (k) \| \forall x \in {Base}_{k} (x \leq_{k} w \to f (x) = x)\}))$
26	0 25	wceq	$wff LDil = (k \in V ⟼ (w \in LHyp (k) ⟼ \{f \in LAut (k) \| \forall x \in {Base}_{k} (x \leq_{k} w \to f (x) = x)\}))$

Metamath Proof Explorer