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