Theorem unopn

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

	Ref	Expression
Assertion	unopn	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\wedge B\in J\right)\to A\cup B\in J$$

Proof

Step	Hyp	Ref	Expression
1		uniprg	$$⊢\left(A\in J\wedge B\in J\right)\to \bigcup \left\{A,B\right\}=A\cup B$$
2	1	3adant1	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\wedge B\in J\right)\to \bigcup \left\{A,B\right\}=A\cup B$$
3		prssi	$$⊢\left(A\in J\wedge B\in J\right)\to \left\{A,B\right\}\subseteq J$$
4		uniopn	$$⊢\left(J\in \mathrm{Top}\wedge \left\{A,B\right\}\subseteq J\right)\to \bigcup \left\{A,B\right\}\in J$$
5	3 4	sylan2	$$⊢\left(J\in \mathrm{Top}\wedge \left(A\in J\wedge B\in J\right)\right)\to \bigcup \left\{A,B\right\}\in J$$
6	5	3impb	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\wedge B\in J\right)\to \bigcup \left\{A,B\right\}\in J$$
7	2 6	eqeltrrd	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\wedge B\in J\right)\to A\cup B\in J$$