Theorem iincld

Description: The indexed intersection of a collection B ( x ) of closed sets is closed. Theorem 6.1(2) of Munkres p. 93. (Contributed by NM, 5-Oct-2006) (Revised by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	iincld	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in \mathrm{Clsd}\left(J\right)\right)\to \bigcap _{x\in A}B\in \mathrm{Clsd}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup J=\bigcup J$$
2	1	cldss	$$⊢B\in \mathrm{Clsd}\left(J\right)\to B\subseteq \bigcup J$$
3		dfss4	$$⊢B\subseteq \bigcup J\leftrightarrow \bigcup J\setminus \left(\bigcup J\setminus B\right)=B$$
4	2 3	sylib	$$⊢B\in \mathrm{Clsd}\left(J\right)\to \bigcup J\setminus \left(\bigcup J\setminus B\right)=B$$
5	4	ralimi	$$⊢\forall x\in AB\in \mathrm{Clsd}\left(J\right)\to \forall x\in A\bigcup J\setminus \left(\bigcup J\setminus B\right)=B$$
6		iineq2	$$⊢\forall x\in A\bigcup J\setminus \left(\bigcup J\setminus B\right)=B\to \bigcap _{x\in A}\left(\bigcup J\setminus \left(\bigcup J\setminus B\right)\right)=\bigcap _{x\in A}B$$
7	5 6	syl	$$⊢\forall x\in AB\in \mathrm{Clsd}\left(J\right)\to \bigcap _{x\in A}\left(\bigcup J\setminus \left(\bigcup J\setminus B\right)\right)=\bigcap _{x\in A}B$$
8	7	adantl	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in \mathrm{Clsd}\left(J\right)\right)\to \bigcap _{x\in A}\left(\bigcup J\setminus \left(\bigcup J\setminus B\right)\right)=\bigcap _{x\in A}B$$
9		iindif2	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left(\bigcup J\setminus \left(\bigcup J\setminus B\right)\right)=\bigcup J\setminus \bigcup _{x\in A}\left(\bigcup J\setminus B\right)$$
10	9	adantr	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in \mathrm{Clsd}\left(J\right)\right)\to \bigcap _{x\in A}\left(\bigcup J\setminus \left(\bigcup J\setminus B\right)\right)=\bigcup J\setminus \bigcup _{x\in A}\left(\bigcup J\setminus B\right)$$
11	8 10	eqtr3d	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in \mathrm{Clsd}\left(J\right)\right)\to \bigcap _{x\in A}B=\bigcup J\setminus \bigcup _{x\in A}\left(\bigcup J\setminus B\right)$$
12		r19.2z	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in \mathrm{Clsd}\left(J\right)\right)\to \exists x\in AB\in \mathrm{Clsd}\left(J\right)$$
13		cldrcl	$$⊢B\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{Top}$$
14	13	rexlimivw	$$⊢\exists x\in AB\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{Top}$$
15	12 14	syl	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in \mathrm{Clsd}\left(J\right)\right)\to J\in \mathrm{Top}$$
16	1	cldopn	$$⊢B\in \mathrm{Clsd}\left(J\right)\to \bigcup J\setminus B\in J$$
17	16	ralimi	$$⊢\forall x\in AB\in \mathrm{Clsd}\left(J\right)\to \forall x\in A\bigcup J\setminus B\in J$$
18	17	adantl	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in \mathrm{Clsd}\left(J\right)\right)\to \forall x\in A\bigcup J\setminus B\in J$$
19		iunopn	$$⊢\left(J\in \mathrm{Top}\wedge \forall x\in A\bigcup J\setminus B\in J\right)\to \bigcup _{x\in A}\left(\bigcup J\setminus B\right)\in J$$
20	15 18 19	syl2anc	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in \mathrm{Clsd}\left(J\right)\right)\to \bigcup _{x\in A}\left(\bigcup J\setminus B\right)\in J$$
21	1	opncld	$$⊢\left(J\in \mathrm{Top}\wedge \bigcup _{x\in A}\left(\bigcup J\setminus B\right)\in J\right)\to \bigcup J\setminus \bigcup _{x\in A}\left(\bigcup J\setminus B\right)\in \mathrm{Clsd}\left(J\right)$$
22	15 20 21	syl2anc	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in \mathrm{Clsd}\left(J\right)\right)\to \bigcup J\setminus \bigcup _{x\in A}\left(\bigcup J\setminus B\right)\in \mathrm{Clsd}\left(J\right)$$
23	11 22	eqeltrd	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in \mathrm{Clsd}\left(J\right)\right)\to \bigcap _{x\in A}B\in \mathrm{Clsd}\left(J\right)$$