This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )