This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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