Metamath Proof Explorer

Theorem tgss

Description: Subset relation for generated topologies. (Contributed by NM, 7-May-2007)

Ref Expression
Assertion tgss ⊢ C ∈ V ∧ B ⊆ C → topGen ⁡ B ⊆ topGen ⁡ C

Proof

Step Hyp Ref Expression
1 ssrin ⊢ B ⊆ C → B ∩ 𝒫 x ⊆ C ∩ 𝒫 x
2 1 unissd ⊢ B ⊆ C → ⋃ B ∩ 𝒫 x ⊆ ⋃ C ∩ 𝒫 x
3 sstr2 ⊢ x ⊆ ⋃ B ∩ 𝒫 x → ⋃ B ∩ 𝒫 x ⊆ ⋃ C ∩ 𝒫 x → x ⊆ ⋃ C ∩ 𝒫 x
4 2 3 syl5com ⊢ B ⊆ C → x ⊆ ⋃ B ∩ 𝒫 x → x ⊆ ⋃ C ∩ 𝒫 x
5 4 adantl ⊢ C ∈ V ∧ B ⊆ C → x ⊆ ⋃ B ∩ 𝒫 x → x ⊆ ⋃ C ∩ 𝒫 x
6 ssexg ⊢ B ⊆ C ∧ C ∈ V → B ∈ V
7 6 ancoms ⊢ C ∈ V ∧ B ⊆ C → B ∈ V
8 eltg ⊢ B ∈ V → x ∈ topGen ⁡ B ↔ x ⊆ ⋃ B ∩ 𝒫 x
9 7 8 syl ⊢ C ∈ V ∧ B ⊆ C → x ∈ topGen ⁡ B ↔ x ⊆ ⋃ B ∩ 𝒫 x
10 eltg ⊢ C ∈ V → x ∈ topGen ⁡ C ↔ x ⊆ ⋃ C ∩ 𝒫 x
11 10 adantr ⊢ C ∈ V ∧ B ⊆ C → x ∈ topGen ⁡ C ↔ x ⊆ ⋃ C ∩ 𝒫 x
12 5 9 11 3imtr4d ⊢ C ∈ V ∧ B ⊆ C → x ∈ topGen ⁡ B → x ∈ topGen ⁡ C
13 12 ssrdv ⊢ C ∈ V ∧ B ⊆ C → topGen ⁡ B ⊆ topGen ⁡ C