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

Definition df-lat 14475
 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 14474 . 2
2 vx . . . . . . . . 9
32cv 1651 . . . . . . . 8
4 vy . . . . . . . . 9
54cv 1651 . . . . . . . 8
6 vp . . . . . . . . . 10
76cv 1651 . . . . . . . . 9
8 cjn 14401 . . . . . . . . 9
97, 8cfv 5454 . . . . . . . 8
103, 5, 9co 6081 . . . . . . 7
11 cbs 13469 . . . . . . . 8
127, 11cfv 5454 . . . . . . 7
1310, 12wcel 1725 . . . . . 6
14 cmee 14402 . . . . . . . . 9
157, 14cfv 5454 . . . . . . . 8
163, 5, 15co 6081 . . . . . . 7
1716, 12wcel 1725 . . . . . 6
1813, 17wa 359 . . . . 5
1918, 4, 12wral 2705 . . . 4
2019, 2, 12wral 2705 . . 3
21 cpo 14397 . . 3
2220, 6, 21crab 2709 . 2
231, 22wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  islat  14476
 Copyright terms: Public domain W3C validator