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 ∈ Top ∧ A ∈ J ∧ B ∈ J → A ∪ B ∈ J

Proof

Step Hyp Ref Expression
1 uniprg ⊢ A ∈ J ∧ B ∈ J → ⋃ A B = A ∪ B
2 1 3adant1 ⊢ J ∈ Top ∧ A ∈ J ∧ B ∈ J → ⋃ A B = A ∪ B
3 prssi ⊢ A ∈ J ∧ B ∈ J → A B ⊆ J
4 uniopn ⊢ J ∈ Top ∧ A B ⊆ J → ⋃ A B ∈ J
5 3 4 sylan2 ⊢ J ∈ Top ∧ A ∈ J ∧ B ∈ J → ⋃ A B ∈ J
6 5 3impb ⊢ J ∈ Top ∧ A ∈ J ∧ B ∈ J → ⋃ A B ∈ J
7 2 6 eqeltrrd ⊢ J ∈ Top ∧ A ∈ J ∧ B ∈ J → A ∪ B ∈ J