# Metamath Proof Explorer

## 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 ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \bigcup {A}\in \mathrm{topGen}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to {A}\subseteq {B}$
2 pwuni ${⊢}{A}\subseteq 𝒫\bigcup {A}$
3 ssin ${⊢}\left({A}\subseteq {B}\wedge {A}\subseteq 𝒫\bigcup {A}\right)↔{A}\subseteq {B}\cap 𝒫\bigcup {A}$
4 1 2 3 sylanblc ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to {A}\subseteq {B}\cap 𝒫\bigcup {A}$
5 4 unissd ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \bigcup {A}\subseteq \bigcup \left({B}\cap 𝒫\bigcup {A}\right)$
6 eltg ${⊢}{B}\in {V}\to \left(\bigcup {A}\in \mathrm{topGen}\left({B}\right)↔\bigcup {A}\subseteq \bigcup \left({B}\cap 𝒫\bigcup {A}\right)\right)$
7 6 adantr ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \left(\bigcup {A}\in \mathrm{topGen}\left({B}\right)↔\bigcup {A}\subseteq \bigcup \left({B}\cap 𝒫\bigcup {A}\right)\right)$
8 5 7 mpbird ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \bigcup {A}\in \mathrm{topGen}\left({B}\right)$