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}}_{\mathscr{H}}$$
	chjcl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		chjcl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
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}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)$$
7	3 4	prss	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\leftrightarrow \left\{A,B\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
8	6 7	mpbi	$$⊢\left\{A,B\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
9	3	prnz	$$⊢\left\{A,B\right\}\ne \varnothing$$
10	8 9	pm3.2i	$$⊢\left(\left\{A,B\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge \left\{A,B\right\}\ne \varnothing \right)$$
11	10	chintcli	$$⊢\bigcap \left\{A,B\right\}\in {\mathbf{C}}_{\mathscr{H}}$$
12	5 11	eqeltrri	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$