Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > latmcl | Structured version Visualization version GIF version | ||
| Description: Closure of meet operation in a lattice. (incom 4202 analog.) (Contributed by NM, 14-Sep-2011.) |
| Ref | Expression |
|---|---|
| latmcl.b | β’ π΅ = (BaseβπΎ) |
| latmcl.m | β’ β§ = (meetβπΎ) |
| Ref | Expression |
|---|---|
| latmcl | β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | latmcl.b | . . 3 β’ π΅ = (BaseβπΎ) | |
| 2 | eqid 2730 | . . 3 β’ (joinβπΎ) = (joinβπΎ) | |
| 3 | latmcl.m | . . 3 β’ β§ = (meetβπΎ) | |
| 4 | 1, 2, 3 | latlem 18396 | . 2 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β ((π(joinβπΎ)π) β π΅ β§ (π β§ π) β π΅)) |
| 5 | 4 | simprd 494 | 1 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
| Copyright terms: Public domain | W3C validator |