Theorem chincli

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

	Ref	Expression
Hypotheses	ch0le.1	|- A e. CH
	chjcl.2	|- B e. CH
Assertion	chincli	|- ( A i^i B ) e. CH

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	|- A e. CH
2		chjcl.2	|- B e. CH
3	1	elexi	|- A e. _V
4	2	elexi	|- B e. _V
5	3 4	intpr	|- |^| { A , B } = ( A i^i B )
6	1 2	pm3.2i	|- ( A e. CH /\ B e. CH )
7	3 4	prss	|- ( ( A e. CH /\ B e. CH ) <-> { A , B } C_ CH )
8	6 7	mpbi	|- { A , B } C_ CH
9	3	prnz	|- { A , B } =/= (/)
10	8 9	pm3.2i	|- ( { A , B } C_ CH /\ { A , B } =/= (/) )
11	10	chintcli	|- |^| { A , B } e. CH
12	5 11	eqeltrri	|- ( A i^i B ) e. CH