Theorem shincli

Description: Closure of intersection of two subspaces. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shincl.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
	shincl.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shincli	$$⊢A\cap B\in {\mathbf{S}}_{\mathscr{H}}$$

Proof

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