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=kVwLHypkfLDilkw|pAtomskqAtomsk¬pkw¬qkwpjoinkfpmeetkw=qjoinkfqmeetkw

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltrn classLTrn
1 vk setvark
2 cvv classV
3 vw setvarw
4 clh classLHyp
5 1 cv setvark
6 5 4 cfv classLHypk
7 vf setvarf
8 cldil classLDil
9 5 8 cfv classLDilk
10 3 cv setvarw
11 10 9 cfv classLDilkw
12 vp setvarp
13 catm classAtoms
14 5 13 cfv classAtomsk
15 vq setvarq
16 12 cv setvarp
17 cple classle
18 5 17 cfv classk
19 16 10 18 wbr wffpkw
20 19 wn wff¬pkw
21 15 cv setvarq
22 21 10 18 wbr wffqkw
23 22 wn wff¬qkw
24 20 23 wa wff¬pkw¬qkw
25 cjn classjoin
26 5 25 cfv classjoink
27 7 cv setvarf
28 16 27 cfv classfp
29 16 28 26 co classpjoinkfp
30 cmee classmeet
31 5 30 cfv classmeetk
32 29 10 31 co classpjoinkfpmeetkw
33 21 27 cfv classfq
34 21 33 26 co classqjoinkfq
35 34 10 31 co classqjoinkfqmeetkw
36 32 35 wceq wffpjoinkfpmeetkw=qjoinkfqmeetkw
37 24 36 wi wff¬pkw¬qkwpjoinkfpmeetkw=qjoinkfqmeetkw
38 37 15 14 wral wffqAtomsk¬pkw¬qkwpjoinkfpmeetkw=qjoinkfqmeetkw
39 38 12 14 wral wffpAtomskqAtomsk¬pkw¬qkwpjoinkfpmeetkw=qjoinkfqmeetkw
40 39 7 11 crab classfLDilkw|pAtomskqAtomsk¬pkw¬qkwpjoinkfpmeetkw=qjoinkfqmeetkw
41 3 6 40 cmpt classwLHypkfLDilkw|pAtomskqAtomsk¬pkw¬qkwpjoinkfpmeetkw=qjoinkfqmeetkw
42 1 2 41 cmpt classkVwLHypkfLDilkw|pAtomskqAtomsk¬pkw¬qkwpjoinkfpmeetkw=qjoinkfqmeetkw
43 0 42 wceq wffLTrn=kVwLHypkfLDilkw|pAtomskqAtomsk¬pkw¬qkwpjoinkfpmeetkw=qjoinkfqmeetkw