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

Definition df-clat 14537
 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 14536 . 2
2 vs . . . . . . 7
32cv 1651 . . . . . 6
4 vp . . . . . . . 8
54cv 1651 . . . . . . 7
6 cbs 13469 . . . . . . 7
75, 6cfv 5454 . . . . . 6
83, 7wss 3320 . . . . 5
9 club 14399 . . . . . . . . 9
105, 9cfv 5454 . . . . . . . 8
113, 10cfv 5454 . . . . . . 7
1211, 7wcel 1725 . . . . . 6
13 cglb 14400 . . . . . . . . 9
145, 13cfv 5454 . . . . . . . 8
153, 14cfv 5454 . . . . . . 7
1615, 7wcel 1725 . . . . . 6
1712, 16wa 359 . . . . 5
188, 17wi 4 . . . 4
1918, 2wal 1549 . . 3
20 cpo 14397 . . 3
2119, 4, 20crab 2709 . 2
221, 21wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  isclat  14538
 Copyright terms: Public domain W3C validator