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