# Metamath Proof Explorer

## Theorem chincli

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

Ref Expression
Hypotheses ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion chincli ${⊢}{A}\cap {B}\in {\mathbf{C}}_{ℋ}$

### Proof

Step Hyp Ref Expression
1 ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 1 elexi ${⊢}{A}\in \mathrm{V}$
4 2 elexi ${⊢}{B}\in \mathrm{V}$
5 3 4 intpr ${⊢}\bigcap \left\{{A},{B}\right\}={A}\cap {B}$
6 1 2 pm3.2i ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)$
7 3 4 prss ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)↔\left\{{A},{B}\right\}\subseteq {\mathbf{C}}_{ℋ}$
8 6 7 mpbi ${⊢}\left\{{A},{B}\right\}\subseteq {\mathbf{C}}_{ℋ}$
9 3 prnz ${⊢}\left\{{A},{B}\right\}\ne \varnothing$
10 8 9 pm3.2i ${⊢}\left(\left\{{A},{B}\right\}\subseteq {\mathbf{C}}_{ℋ}\wedge \left\{{A},{B}\right\}\ne \varnothing \right)$
11 10 chintcli ${⊢}\bigcap \left\{{A},{B}\right\}\in {\mathbf{C}}_{ℋ}$
12 5 11 eqeltrri ${⊢}{A}\cap {B}\in {\mathbf{C}}_{ℋ}$