Theorem unopn

Description: The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	unopn	|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A u. B ) e. J )

Proof

Step	Hyp	Ref	Expression
1		uniprg	|- ( ( A e. J /\ B e. J ) -> U. { A , B } = ( A u. B ) )
2	1	3adant1	|- ( ( J e. Top /\ A e. J /\ B e. J ) -> U. { A , B } = ( A u. B ) )
3		prssi	|- ( ( A e. J /\ B e. J ) -> { A , B } C_ J )
4		uniopn	|- ( ( J e. Top /\ { A , B } C_ J ) -> U. { A , B } e. J )
5	3 4	sylan2	|- ( ( J e. Top /\ ( A e. J /\ B e. J ) ) -> U. { A , B } e. J )
6	5	3impb	|- ( ( J e. Top /\ A e. J /\ B e. J ) -> U. { A , B } e. J )
7	2 6	eqeltrrd	|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A u. B ) e. J )