Theorem chintcli

Description: The intersection of a nonempty set of closed subspaces is a closed subspace. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	chintcl.1	$$⊢\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right)$$
Assertion	chintcli	$$⊢\bigcap A\in {\mathbf{C}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		chintcl.1	$$⊢\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge A\ne \varnothing \right)$$
2	1	simpli	$$⊢A\subseteq {\mathbf{C}}_{\mathscr{H}}$$
3		chsssh	$$⊢{\mathbf{C}}_{\mathscr{H}}\subseteq {\mathbf{S}}_{\mathscr{H}}$$
4	2 3	sstri	$$⊢A\subseteq {\mathbf{S}}_{\mathscr{H}}$$
5	1	simpri	$$⊢A\ne \varnothing$$
6	4 5	pm3.2i	$$⊢\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge A\ne \varnothing \right)$$
7	6	shintcli	$$⊢\bigcap A\in {\mathbf{S}}_{\mathscr{H}}$$
8	2	sseli	$$⊢y\in A\to y\in {\mathbf{C}}_{\mathscr{H}}$$
9		vex	$$⊢x\in \mathrm{V}$$
10	9	chlimi	$$⊢\left(y\in {\mathbf{C}}_{\mathscr{H}}\wedge f:\mathbb{N}⟶y\wedge f\underset{v}{⇝}x\right)\to x\in y$$
11	10	3exp	$$⊢y\in {\mathbf{C}}_{\mathscr{H}}\to \left(f:\mathbb{N}⟶y\to \left(f\underset{v}{⇝}x\to x\in y\right)\right)$$
12	11	com3r	$$⊢f\underset{v}{⇝}x\to \left(y\in {\mathbf{C}}_{\mathscr{H}}\to \left(f:\mathbb{N}⟶y\to x\in y\right)\right)$$
13	8 12	syl5	$$⊢f\underset{v}{⇝}x\to \left(y\in A\to \left(f:\mathbb{N}⟶y\to x\in y\right)\right)$$
14	13	imp	$$⊢\left(f\underset{v}{⇝}x\wedge y\in A\right)\to \left(f:\mathbb{N}⟶y\to x\in y\right)$$
15	14	ralimdva	$$⊢f\underset{v}{⇝}x\to \left(\forall y\in Af:\mathbb{N}⟶y\to \forall y\in Ax\in y\right)$$
16	5	fint	$$⊢f:\mathbb{N}⟶\bigcap A\leftrightarrow \forall y\in Af:\mathbb{N}⟶y$$
17	9	elint2	$$⊢x\in \bigcap A\leftrightarrow \forall y\in Ax\in y$$
18	15 16 17	3imtr4g	$$⊢f\underset{v}{⇝}x\to \left(f:\mathbb{N}⟶\bigcap A\to x\in \bigcap A\right)$$
19	18	impcom	$$⊢\left(f:\mathbb{N}⟶\bigcap A\wedge f\underset{v}{⇝}x\right)\to x\in \bigcap A$$
20	19	gen2	$$⊢\forall f\forall x\left(\left(f:\mathbb{N}⟶\bigcap A\wedge f\underset{v}{⇝}x\right)\to x\in \bigcap A\right)$$
21		isch2	$$⊢\bigcap A\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow \left(\bigcap A\in {\mathbf{S}}_{\mathscr{H}}\wedge \forall f\forall x\left(\left(f:\mathbb{N}⟶\bigcap A\wedge f\underset{v}{⇝}x\right)\to x\in \bigcap A\right)\right)$$
22	7 20 21	mpbir2an	$$⊢\bigcap A\in {\mathbf{C}}_{\mathscr{H}}$$