# Metamath Proof Explorer

## 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}}_{ℋ}$
shincl.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
Assertion shincli ${⊢}{A}\cap {B}\in {\mathbf{S}}_{ℋ}$

### Proof

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