Theorem eltg3i

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

	Ref	Expression
Assertion	eltg3i	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) → ∪ 𝐴 ∈ ( topGen ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ 𝐵 )
2		pwuni	⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
3		ssin	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝒫 ∪ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐵 ∩ 𝒫 ∪ 𝐴 ) )
4	1 2 3	sylanblc	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ ( 𝐵 ∩ 𝒫 ∪ 𝐴 ) )
5	4	unissd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) → ∪ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 ∪ 𝐴 ) )
6		eltg	⊢ ( 𝐵 ∈ 𝑉 → ( ∪ 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ∪ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 ∪ 𝐴 ) ) )
7	6	adantr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) → ( ∪ 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ∪ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 ∪ 𝐴 ) ) )
8	5 7	mpbird	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) → ∪ 𝐴 ∈ ( topGen ‘ 𝐵 ) )