This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tgss

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

Ref Expression
Assertion tgss ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ssrin ⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ( 𝐶 ∩ 𝒫 𝑥 ) )
2 1 unissd ⊢ ( 𝐵 ⊆ 𝐶 → ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) )
3 sstr2 ⊢ ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → ( ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) ) )
4 2 3 syl5com ⊢ ( 𝐵 ⊆ 𝐶 → ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) ) )
5 4 adantl ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) ) )
6 ssexg ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ∈ 𝑉 ) → 𝐵 ∈ V )
7 6 ancoms ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → 𝐵 ∈ V )
8 eltg ⊢ ( 𝐵 ∈ V → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
9 7 8 syl ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
10 eltg ⊢ ( 𝐶 ∈ 𝑉 → ( 𝑥 ∈ ( topGen ‘ 𝐶 ) ↔ 𝑥 ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) ) )
11 10 adantr ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ∈ ( topGen ‘ 𝐶 ) ↔ 𝑥 ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) ) )
12 5 9 11 3imtr4d ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) → 𝑥 ∈ ( topGen ‘ 𝐶 ) ) )
13 12 ssrdv ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) )