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

Definition df-dlat 14618
 Description: A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 14616) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
Assertion
Ref Expression
df-dlat DLat
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-dlat
StepHypRef Expression
1 cdlat 14617 . 2 DLat
2 vx . . . . . . . . . . . 12
32cv 1651 . . . . . . . . . . 11
4 vy . . . . . . . . . . . . 13
54cv 1651 . . . . . . . . . . . 12
6 vz . . . . . . . . . . . . 13
76cv 1651 . . . . . . . . . . . 12
8 vj . . . . . . . . . . . . 13
98cv 1651 . . . . . . . . . . . 12
105, 7, 9co 6081 . . . . . . . . . . 11
11 vm . . . . . . . . . . . 12
1211cv 1651 . . . . . . . . . . 11
133, 10, 12co 6081 . . . . . . . . . 10
143, 5, 12co 6081 . . . . . . . . . . 11
153, 7, 12co 6081 . . . . . . . . . . 11
1614, 15, 9co 6081 . . . . . . . . . 10
1713, 16wceq 1652 . . . . . . . . 9
18 vb . . . . . . . . . 10
1918cv 1651 . . . . . . . . 9
2017, 6, 19wral 2705 . . . . . . . 8
2120, 4, 19wral 2705 . . . . . . 7
2221, 2, 19wral 2705 . . . . . 6
23 vk . . . . . . . 8
2423cv 1651 . . . . . . 7
25 cmee 14402 . . . . . . 7
2624, 25cfv 5454 . . . . . 6
2722, 11, 26wsbc 3161 . . . . 5
28 cjn 14401 . . . . . 6
2924, 28cfv 5454 . . . . 5
3027, 8, 29wsbc 3161 . . . 4
31 cbs 13469 . . . . 5
3224, 31cfv 5454 . . . 4
3330, 18, 32wsbc 3161 . . 3
34 clat 14474 . . 3
3533, 23, 34crab 2709 . 2
361, 35wceq 1652 1 DLat
 Colors of variables: wff set class This definition is referenced by:  isdlat  14619
 Copyright terms: Public domain W3C validator