**Description:** Closure of join operation in a lattice. ( chjcom analog.)
(Contributed by NM, 14-Sep-2011)

Ref | Expression | ||
---|---|---|---|

Hypotheses | latjcl.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |

latjcl.j | ⊢ ∨ = ( join ‘ 𝐾 ) | ||

Assertion | latjcl | ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | latjcl.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |

2 | latjcl.j | ⊢ ∨ = ( join ‘ 𝐾 ) | |

3 | eqid | ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) | |

4 | 1 2 3 | latlem | ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ) ) |

5 | 4 | simpld | ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) |