Metamath Proof Explorer

Definition df-ltrn

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

Ref Expression
Assertion df-ltrn ⊢ LTrn = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LDil ⁡ k ⁡ w | ∀ p ∈ Atoms ⁡ k ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltrn class LTrn
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 cldil class LDil
9 5 8 cfv class LDil ⁡ k
10 3 cv setvar w
11 10 9 cfv class LDil ⁡ k ⁡ w
12 vp setvar p
13 catm class Atoms
14 5 13 cfv class Atoms ⁡ k
15 vq setvar q
16 12 cv setvar p
17 cple class le
18 5 17 cfv class ≤ k
19 16 10 18 wbr wff p ≤ k w
20 19 wn wff ¬ p ≤ k w
21 15 cv setvar q
22 21 10 18 wbr wff q ≤ k w
23 22 wn wff ¬ q ≤ k w
24 20 23 wa wff ¬ p ≤ k w ∧ ¬ q ≤ k w
25 cjn class join
26 5 25 cfv class join ⁡ k
27 7 cv setvar f
28 16 27 cfv class f ⁡ p
29 16 28 26 co class p join ⁡ k f ⁡ p
30 cmee class meet
31 5 30 cfv class meet ⁡ k
32 29 10 31 co class p join ⁡ k f ⁡ p meet ⁡ k w
33 21 27 cfv class f ⁡ q
34 21 33 26 co class q join ⁡ k f ⁡ q
35 34 10 31 co class q join ⁡ k f ⁡ q meet ⁡ k w
36 32 35 wceq wff p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w
37 24 36 wi wff ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w
38 37 15 14 wral wff ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w
39 38 12 14 wral wff ∀ p ∈ Atoms ⁡ k ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w
40 39 7 11 crab class f ∈ LDil ⁡ k ⁡ w | ∀ p ∈ Atoms ⁡ k ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w
41 3 6 40 cmpt class w ∈ LHyp ⁡ k ⟼ f ∈ LDil ⁡ k ⁡ w | ∀ p ∈ Atoms ⁡ k ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w
42 1 2 41 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LDil ⁡ k ⁡ w | ∀ p ∈ Atoms ⁡ k ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w
43 0 42 wceq wff LTrn = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LDil ⁡ k ⁡ w | ∀ p ∈ Atoms ⁡ k ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w