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

Metamath Proof Explorer

Theorem iunopn

Description: The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006)

Ref Expression
Assertion iunopn ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 dfiun2g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
2 1 adantl ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
3 uniiunlem ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐽 ) )
4 3 ibi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐽 )
5 uniopn ⊢ ( ( 𝐽 ∈ Top ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐽 ) → ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ 𝐽 )
6 4 5 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) → ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ 𝐽 )
7 2 6 eqeltrd ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 )