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 ⊢ J ∈ Top ∧ A ⊆ J → ⋃ A ∈ J

Proof

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