Metamath Proof Explorer

Theorem tgiun

Description: The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion tgiun ⊢ B ∈ V ∧ ∀ x ∈ A C ∈ B → ⋃ x ∈ A C ∈ topGen ⁡ B

Proof

Step Hyp Ref Expression
1 dfiun3g ⊢ ∀ x ∈ A C ∈ B → ⋃ x ∈ A C = ⋃ ran ⁡ x ∈ A ⟼ C
2 1 adantl ⊢ B ∈ V ∧ ∀ x ∈ A C ∈ B → ⋃ x ∈ A C = ⋃ ran ⁡ x ∈ A ⟼ C
3 eqid ⊢ x ∈ A ⟼ C = x ∈ A ⟼ C
4 3 rnmptss ⊢ ∀ x ∈ A C ∈ B → ran ⁡ x ∈ A ⟼ C ⊆ B
5 eltg3i ⊢ B ∈ V ∧ ran ⁡ x ∈ A ⟼ C ⊆ B → ⋃ ran ⁡ x ∈ A ⟼ C ∈ topGen ⁡ B
6 4 5 sylan2 ⊢ B ∈ V ∧ ∀ x ∈ A C ∈ B → ⋃ ran ⁡ x ∈ A ⟼ C ∈ topGen ⁡ B
7 2 6 eqeltrd ⊢ B ∈ V ∧ ∀ x ∈ A C ∈ B → ⋃ x ∈ A C ∈ topGen ⁡ B