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

Definition df-lar 14638
 Description: Define the class of all lattices, which are posets in which every two elements have upper and lower bounds. (Contributed by NM, 12-Jun-2008.)
Assertion
Ref Expression
df-lar
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-lar
StepHypRef Expression
1 cla 14633 . 2
2 vr . . . . . . . . 9
32cv 1652 . . . . . . . 8
4 vx . . . . . . . . . 10
54cv 1652 . . . . . . . . 9
6 vy . . . . . . . . . 10
76cv 1652 . . . . . . . . 9
85, 7cpr 3817 . . . . . . . 8
9 cspw 14631 . . . . . . . 8
103, 8, 9co 6084 . . . . . . 7
113cdm 4881 . . . . . . 7
1210, 11wcel 1726 . . . . . 6
13 cinf 14632 . . . . . . . 8
143, 8, 13co 6084 . . . . . . 7
1514, 11wcel 1726 . . . . . 6
1612, 15wa 360 . . . . 5
1716, 6, 11wral 2707 . . . 4
1817, 4, 11wral 2707 . . 3
19 cps 14629 . . 3
2018, 2, 19crab 2711 . 2
211, 20wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  isla  14670
 Copyright terms: Public domain W3C validator