Description: The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009)
Ref | Expression | ||
---|---|---|---|
Assertion | unopn | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝐽 ) |
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 ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝐽 ) |