Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lat Unicode version

Definition df-lat 14430
 Description: Define the class of all lattices. A lattice is a poset in which the join and meet of any two elements always exists. (Contributed by NM, 18-Oct-2012.)
Assertion
Ref Expression
df-lat
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-lat
StepHypRef Expression
1 clat 14429 . 2
2 vx . . . . . . . . 9
32cv 1648 . . . . . . . 8
4 vy . . . . . . . . 9
54cv 1648 . . . . . . . 8
6 vp . . . . . . . . . 10
76cv 1648 . . . . . . . . 9
8 cjn 14356 . . . . . . . . 9
97, 8cfv 5413 . . . . . . . 8
103, 5, 9co 6040 . . . . . . 7
11 cbs 13424 . . . . . . . 8
127, 11cfv 5413 . . . . . . 7
1310, 12wcel 1721 . . . . . 6
14 cmee 14357 . . . . . . . . 9
157, 14cfv 5413 . . . . . . . 8
163, 5, 15co 6040 . . . . . . 7
1716, 12wcel 1721 . . . . . 6
1813, 17wa 359 . . . . 5
1918, 4, 12wral 2666 . . . 4
2019, 2, 12wral 2666 . . 3
21 cpo 14352 . . 3
2220, 6, 21crab 2670 . 2
231, 22wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  islat  14431
 Copyright terms: Public domain W3C validator