Theorem uniopn

Description: The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006)

	Ref	Expression
Assertion	uniopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ∪ 𝐴 ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		istopg	⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 ) ) )
2	1	ibi	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 ) )
3	2	simpld	⊢ ( 𝐽 ∈ Top → ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) )
4		elpw2g	⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ 𝒫 𝐽 ↔ 𝐴 ⊆ 𝐽 ) )
5	4	biimpar	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → 𝐴 ∈ 𝒫 𝐽 )
6		sseq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝐽 ↔ 𝐴 ⊆ 𝐽 ) )
7		unieq	⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 )
8	7	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ∪ 𝑥 ∈ 𝐽 ↔ ∪ 𝐴 ∈ 𝐽 ) )
9	6 8	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) ↔ ( 𝐴 ⊆ 𝐽 → ∪ 𝐴 ∈ 𝐽 ) ) )
10	9	spcgv	⊢ ( 𝐴 ∈ 𝒫 𝐽 → ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) → ( 𝐴 ⊆ 𝐽 → ∪ 𝐴 ∈ 𝐽 ) ) )
11	5 10	syl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) → ( 𝐴 ⊆ 𝐽 → ∪ 𝐴 ∈ 𝐽 ) ) )
12	11	com23	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ( 𝐴 ⊆ 𝐽 → ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) → ∪ 𝐴 ∈ 𝐽 ) ) )
13	12	ex	⊢ ( 𝐽 ∈ Top → ( 𝐴 ⊆ 𝐽 → ( 𝐴 ⊆ 𝐽 → ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) → ∪ 𝐴 ∈ 𝐽 ) ) ) )
14	13	pm2.43d	⊢ ( 𝐽 ∈ Top → ( 𝐴 ⊆ 𝐽 → ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) → ∪ 𝐴 ∈ 𝐽 ) ) )
15	3 14	mpid	⊢ ( 𝐽 ∈ Top → ( 𝐴 ⊆ 𝐽 → ∪ 𝐴 ∈ 𝐽 ) )
16	15	imp	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ∪ 𝐴 ∈ 𝐽 )