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 ‘ 𝐶 ) )