Theorem shintcl

Description: The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	shintcl	$$⊢\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right)\to \bigcap A\in {\mathbf{S}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		inteq	$$⊢A=if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\to \bigcap A=\bigcap if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)$$
2	1	eleq1d	$$⊢A=if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\to \left(\bigcap A\in {\mathbf{S}}_{\mathscr{H}}\leftrightarrow \bigcap if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\in {\mathbf{S}}_{\mathscr{H}}\right)$$
3		sseq1	$$⊢A=if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\to \left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\leftrightarrow if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\subseteq {\mathbf{S}}_{\mathscr{H}}\right)$$
4		neeq1	$$⊢A=if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\to \left(A\ne \varnothing \leftrightarrow if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\ne \varnothing \right)$$
5	3 4	anbi12d	$$⊢A=if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\to \left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right)\leftrightarrow \left(if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\ne \varnothing \right)\right)$$
6		sseq1	$$⊢{\mathbf{S}}_{\mathscr{H}}=if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\to \left({\mathbf{S}}_{\mathscr{H}}\subseteq {\mathbf{S}}_{\mathscr{H}}\leftrightarrow if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\subseteq {\mathbf{S}}_{\mathscr{H}}\right)$$
7		neeq1	$$⊢{\mathbf{S}}_{\mathscr{H}}=if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\to \left({\mathbf{S}}_{\mathscr{H}}\ne \varnothing \leftrightarrow if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\ne \varnothing \right)$$
8	6 7	anbi12d	$$⊢{\mathbf{S}}_{\mathscr{H}}=if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\to \left(\left({\mathbf{S}}_{\mathscr{H}}\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge {\mathbf{S}}_{\mathscr{H}}\ne \varnothing \right)\leftrightarrow \left(if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\ne \varnothing \right)\right)$$
9		ssid	$$⊢{\mathbf{S}}_{\mathscr{H}}\subseteq {\mathbf{S}}_{\mathscr{H}}$$
10		h0elsh	$$⊢0_{\mathscr{H}}\in {\mathbf{S}}_{\mathscr{H}}$$
11	10	ne0ii	$$⊢{\mathbf{S}}_{\mathscr{H}}\ne \varnothing$$
12	9 11	pm3.2i	$$⊢\left({\mathbf{S}}_{\mathscr{H}}\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge {\mathbf{S}}_{\mathscr{H}}\ne \varnothing \right)$$
13	5 8 12	elimhyp	$$⊢\left(if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\ne \varnothing \right)$$
14	13	shintcli	$$⊢\bigcap if\left(\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right),A,{\mathbf{S}}_{\mathscr{H}}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
15	2 14	dedth	$$⊢\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right)\to \bigcap A\in {\mathbf{S}}_{\mathscr{H}}$$