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	|- ( ( J e. Top /\ A. x e. A B e. J ) -> U_ x e. A B e. J )

Proof

Step	Hyp	Ref	Expression
1		dfiun2g	|- ( A. x e. A B e. J -> U_ x e. A B = U. { y | E. x e. A y = B } )
2	1	adantl	|- ( ( J e. Top /\ A. x e. A B e. J ) -> U_ x e. A B = U. { y | E. x e. A y = B } )
3		uniiunlem	|- ( A. x e. A B e. J -> ( A. x e. A B e. J <-> { y | E. x e. A y = B } C_ J ) )
4	3	ibi	|- ( A. x e. A B e. J -> { y | E. x e. A y = B } C_ J )
5		uniopn	|- ( ( J e. Top /\ { y | E. x e. A y = B } C_ J ) -> U. { y | E. x e. A y = B } e. J )
6	4 5	sylan2	|- ( ( J e. Top /\ A. x e. A B e. J ) -> U. { y | E. x e. A y = B } e. J )
7	2 6	eqeltrd	|- ( ( J e. Top /\ A. x e. A B e. J ) -> U_ x e. A B e. J )