# Metamath Proof Explorer

## Theorem chincl

Description: Closure of Hilbert lattice intersection. (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chincl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap {B}\in {\mathbf{C}}_{ℋ}$

### Proof

Step Hyp Ref Expression
1 ineq1 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to {A}\cap {B}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap {B}$
2 1 eleq1d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \left({A}\cap {B}\in {\mathbf{C}}_{ℋ}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap {B}\in {\mathbf{C}}_{ℋ}\right)$
3 ineq2 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap {B}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)$
4 3 eleq1d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap {B}\in {\mathbf{C}}_{ℋ}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\in {\mathbf{C}}_{ℋ}\right)$
5 ifchhv ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\in {\mathbf{C}}_{ℋ}$
6 ifchhv ${⊢}if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\in {\mathbf{C}}_{ℋ}$
7 5 6 chincli ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\in {\mathbf{C}}_{ℋ}$
8 2 4 7 dedth2h ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap {B}\in {\mathbf{C}}_{ℋ}$