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

Definition df-clat 14492
 Description: Define the class of all complete lattices. (Contributed by NM, 18-Oct-2012.)
Assertion
Ref Expression
df-clat
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-clat
StepHypRef Expression
1 ccla 14491 . 2
2 vs . . . . . . 7
32cv 1648 . . . . . 6
4 vp . . . . . . . 8
54cv 1648 . . . . . . 7
6 cbs 13424 . . . . . . 7
75, 6cfv 5413 . . . . . 6
83, 7wss 3280 . . . . 5
9 club 14354 . . . . . . . . 9
105, 9cfv 5413 . . . . . . . 8
113, 10cfv 5413 . . . . . . 7
1211, 7wcel 1721 . . . . . 6
13 cglb 14355 . . . . . . . . 9
145, 13cfv 5413 . . . . . . . 8
153, 14cfv 5413 . . . . . . 7
1615, 7wcel 1721 . . . . . 6
1712, 16wa 359 . . . . 5
188, 17wi 4 . . . 4
1918, 2wal 1546 . . 3
20 cpo 14352 . . 3
2119, 4, 20crab 2670 . 2
221, 21wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  isclat  14493
 Copyright terms: Public domain W3C validator