Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlatjcl | Structured version Visualization version GIF version |
Description: Closure of join operation. Frequently-used special case of latjcl 17777 for atoms. (Contributed by NM, 15-Jun-2012.) |
Ref | Expression |
---|---|
hlatjcl.b | ⊢ 𝐵 = (Base‘𝐾) |
hlatjcl.j | ⊢ ∨ = (join‘𝐾) |
hlatjcl.a | ⊢ 𝐴 = (Atoms‘𝐾) |
Ref | Expression |
---|---|
hlatjcl | ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hllat 37000 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | |
2 | hlatjcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
3 | hlatjcl.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | 2, 3 | atbase 36926 | . 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐵) |
5 | 2, 3 | atbase 36926 | . 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ 𝐵) |
6 | hlatjcl.j | . . 3 ⊢ ∨ = (join‘𝐾) | |
7 | 2, 6 | latjcl 17777 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵) |
8 | 1, 4, 5, 7 | syl3an 1161 | 1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵) |
Copyright terms: Public domain | W3C validator |