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 ( ( 𝐽 ∈ Top ∧ 𝐴𝐽𝐵𝐽 ) → ( 𝐴𝐵 ) ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 uniprg ( ( 𝐴𝐽𝐵𝐽 ) → { 𝐴 , 𝐵 } = ( 𝐴𝐵 ) )
2 1 3adant1 ( ( 𝐽 ∈ Top ∧ 𝐴𝐽𝐵𝐽 ) → { 𝐴 , 𝐵 } = ( 𝐴𝐵 ) )
3 prssi ( ( 𝐴𝐽𝐵𝐽 ) → { 𝐴 , 𝐵 } ⊆ 𝐽 )
4 uniopn ( ( 𝐽 ∈ Top ∧ { 𝐴 , 𝐵 } ⊆ 𝐽 ) → { 𝐴 , 𝐵 } ∈ 𝐽 )
5 3 4 sylan2 ( ( 𝐽 ∈ Top ∧ ( 𝐴𝐽𝐵𝐽 ) ) → { 𝐴 , 𝐵 } ∈ 𝐽 )
6 5 3impb ( ( 𝐽 ∈ Top ∧ 𝐴𝐽𝐵𝐽 ) → { 𝐴 , 𝐵 } ∈ 𝐽 )
7 2 6 eqeltrrd ( ( 𝐽 ∈ Top ∧ 𝐴𝐽𝐵𝐽 ) → ( 𝐴𝐵 ) ∈ 𝐽 )