Metamath Proof Explorer

Definition 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 ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LAut ⁡ k | ∀ x ∈ Base k x ≤ k w → f ⁡ x = x

Detailed syntax breakdown

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 ≤ k
16 3 cv setvar w
17 13 16 15 wbr wff x ≤ 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 ≤ k w → f ⁡ x = x
22 21 10 12 wral wff ∀ x ∈ Base k x ≤ k w → f ⁡ x = x
23 22 7 9 crab class f ∈ LAut ⁡ k | ∀ x ∈ Base k x ≤ k w → f ⁡ x = x
24 3 6 23 cmpt class w ∈ LHyp ⁡ k ⟼ f ∈ LAut ⁡ k | ∀ x ∈ Base k x ≤ k w → f ⁡ x = x
25 1 2 24 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LAut ⁡ k | ∀ x ∈ Base k x ≤ k w → f ⁡ x = x
26 0 25 wceq wff LDil = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LAut ⁡ k | ∀ x ∈ Base k x ≤ k w → f ⁡ x = x