Theorem iunopn

Description: The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006)

	Ref	Expression
Assertion	iunopn	$$⊢\left(J\in \mathrm{Top}\wedge \forall x\in AB\in J\right)\to \bigcup _{x\in A}B\in J$$

Proof

Step	Hyp	Ref	Expression
1		dfiun2g	$$⊢\forall x\in AB\in J\to \bigcup _{x\in A}B=\bigcup \left\{y|\exists x\in Ay=B\right\}$$
2	1	adantl	$$⊢\left(J\in \mathrm{Top}\wedge \forall x\in AB\in J\right)\to \bigcup _{x\in A}B=\bigcup \left\{y|\exists x\in Ay=B\right\}$$
3		uniiunlem	$$⊢\forall x\in AB\in J\to \left(\forall x\in AB\in J\leftrightarrow \left\{y|\exists x\in Ay=B\right\}\subseteq J\right)$$
4	3	ibi	$$⊢\forall x\in AB\in J\to \left\{y|\exists x\in Ay=B\right\}\subseteq J$$
5		uniopn	$$⊢\left(J\in \mathrm{Top}\wedge \left\{y|\exists x\in Ay=B\right\}\subseteq J\right)\to \bigcup \left\{y|\exists x\in Ay=B\right\}\in J$$
6	4 5	sylan2	$$⊢\left(J\in \mathrm{Top}\wedge \forall x\in AB\in J\right)\to \bigcup \left\{y|\exists x\in Ay=B\right\}\in J$$
7	2 6	eqeltrd	$$⊢\left(J\in \mathrm{Top}\wedge \forall x\in AB\in J\right)\to \bigcup _{x\in A}B\in J$$