|   | 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 4209 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 2737 | . . 3 ⊢ (join‘𝐾) = (join‘𝐾) | |
| 3 | latmcl.m | . . 3 ⊢ ∧ = (meet‘𝐾) | |
| 4 | 1, 2, 3 | latlem 18482 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵)) | 
| 5 | 4 | simprd 495 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) | 
| Copyright terms: Public domain | W3C validator |